regularity — Mathlib

English

Every nonempty set x contains some y ∈ x such that x ∩ y = ∅.

Русский

Любое непустое множество x содержит элемент y ∈ x такой, что x ∩ y = ∅.

LaTeX

$$$\\forall x\\, (x \\neq \\emptyset) \\Rightarrow \\exists y \\in x, x \\cap y = \\emptyset$$$

Lean4

theorem regularity (x : ZFSet.{u}) (h : x ≠ ∅) : ∃ y ∈ x, x ∩ y = ∅ :=
  by_contradiction fun ne =>
    h <|
      (eq_empty x).2 fun y =>
        @inductionOn (fun z => z ∉ x) y fun z IH zx =>
          ne
            ⟨z, zx,
              (eq_empty _).2 fun w wxz =>
                let ⟨wx, wz⟩ := mem_inter.1 wxz
                IH w wz wx⟩

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