ofSet_eq_refl — Mathlib

English

An equality of ofSet with the identity equivalence holds exactly when s is the entire universe.

Русский

Тождество эквивалента, построенного через s, и тождественный эквивалент выполняются тогда, когда s = Set.univ.

LaTeX

$$$\\operatorname{ofSet} s = PEquiv.refl \\alpha \\iff s = \\mathrm{Set.univ}$$$

Lean4

@[simp]
theorem ofSet_eq_refl {s : Set α} [DecidablePred (· ∈ s)] : ofSet s = PEquiv.refl α ↔ s = Set.univ :=
  ⟨fun h => by
    rw [Set.eq_univ_iff_forall]
    intro
    rw [← mem_ofSet_self_iff, h]
    exact rfl, fun h => by simp only [← ofSet_univ, h]⟩

Похожие утверждения