not_subset_iff_mem

Mathlib.SetTheory.ZFC.Ordinal

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

English

For ordinals x,y, ¬(x ⊆ y) iff y ∈ x.

Русский

Для ординалов x,y: ¬(x ⊆ y) тогда и только тогда, когда y ∈ x.

LaTeX

$$$IsOrdinal(x) \land IsOrdinal(y) \Rightarrow (\lnot (x \subseteq y) \iff y \in x)$$$

Lean4

theorem not_subset_iff_mem (hx : x.IsOrdinal) (hy : y.IsOrdinal) : ¬x ⊆ y ↔ y ∈ x := by
  rw [not_iff_comm, notMem_iff_subset hy hx]

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

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

Разделы

Аффилиация

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