mem_or_subset

Mathlib.SetTheory.ZFC.Ordinal

URI: https://scilib.ai/kg/mathlib#ZFSet.IsOrdinal.mem_or_subset

English

For ordinals x,y, either x ∈ y or y ⊆ x.

Русский

Для ординалов x,y либо x ∈ y, либо y ⊆ x.

LaTeX

$$$IsOrdinal(x) \land IsOrdinal(y) \Rightarrow (x \in y \lor y \subseteq x)$$$

Lean4

theorem mem_or_subset (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ∈ y ∨ y ⊆ x :=
  by
  rw [or_iff_not_imp_left, notMem_iff_subset hx hy]
  exact id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru