α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ (∀ (x : α), x ∈ {a | isSome (↑f a) = true}) ↔ ∀ (a : α), isSome (↑f a) = true
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ PEquiv.trans f (PEquiv.symm f) = PEquiv.refl α ↔ ∀ (a : α), isSome (↑f a) = true
rw [self_trans_symm, ofSet_eq_refl, Set.eq_univ_iff_forall]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ (∀ (x : α), x ∈ {a | isSome (↑f a) = true}) ↔ ∀ (a : α), isSome (↑f a) = true
rfl