def Function.myEquiv {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (f : α → β₁ ⊕ β₂) : α ≃ { x₁ : α × β₁ // f x₁.1 = Sum.inl x₁.2 } ⊕ { x₂ : α × β₂ // f x₂.1 = Sum.inr x₂.2 }

Equations

• One or more equations did not get rendered due to their size.

theorem Function.eq_comp_myEquiv {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (f : α → β₁ ⊕ β₂) : f = Sum.elim (Sum.inl ∘ fun (x : { x₁ : α × β₁ // f x₁.1 = Sum.inl x₁.2 }) => (↑x).2) (Sum.inr ∘ fun (x : { x₂ : α × β₂ // f x₂.1 = Sum.inr x₂.2 }) => (↑x).2) ∘ ⇑(Function.myEquiv f)

theorem zom_mul_zom {R : Type u_1} [Ring R] {x : R} {y : R} (hx : x = 0 ∨ x = 1 ∨ x = -1) (hy : y = 0 ∨ y = 1 ∨ y = -1) : x * y = 0 ∨ x * y = 1 ∨ x * y = -1

theorem abs_eq_one {R : Type u_1} [LinearOrderedCommRing R] (r : R) : |r| = 1 ↔ r = 1 ∨ r = -1