mem_trichotomous

Mathlib.SetTheory.ZFC.Ordinal

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem mem_trichotomous (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ∈ y ∨ x = y ∨ y ∈ x :=
  by
  rw [eq_comm, ← subset_iff_eq_or_mem hy hx]
  exact mem_or_subset hx hy

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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