eq_univ_of_powerset_subset — Mathlib

English

If every subset of a class A is contained in A, then A = univ.

Русский

Если каждый поднабор класса A содержится в A, то A = univ.

LaTeX

$$$ A = \\mathrm{univ} \\quad\\text{если } \\operatorname{powerset}(A) \\subseteq A. $$$

Lean4

/-- An induction principle for sets. If every subset of a class is a member, then the class is
  universal. -/
theorem eq_univ_of_powerset_subset {A : Class} (hA : powerset A ⊆ A) : A = univ :=
  eq_univ_of_forall
    (by
      by_contra! hnA
      exact
        WellFounded.min_mem ZFSet.mem_wf _ hnA
          (hA fun x hx => Classical.not_not.1 fun hB => WellFounded.not_lt_min ZFSet.mem_wf _ hnA hB <| coe_apply.1 hx))

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