notMem_iff_subset — Mathlib

English

For ordinals x,y, x ∉ y iff y ⊆ x.

Русский

Для ординалов x,y: x не является элементом y тогда и только тогда, когда y ⊆ x.

LaTeX

$$$IsOrdinal(x) \land IsOrdinal(y) \Rightarrow (x \notin y \iff y \subseteq x)$$$

Lean4

theorem notMem_iff_subset (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ∉ y ↔ y ⊆ x :=
  by
  refine ⟨?_, fun hxy hyx ↦ mem_irrefl _ (hxy hyx)⟩
  revert hx hy
  apply Sym2.GameAdd.induction mem_wf _ x y
  intro x y IH hx hy hyx z hzy
  by_contra hzx
  exact hyx (mem_of_subset_of_mem hx hy (IH z x (Sym2.GameAdd.fst_snd hzy) (hy.mem hzy) hx hzx) hzy)

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