singleton_mem_subchain_iff

Mathlib.Order.Height

URI: https://scilib.ai/kg/mathlib#Set.singleton_mem_subchain_iff

English

For any a in α, [a] ∈ s.subchain iff a ∈ s.

Русский

Для любого элемента a ∈ α, список [a] принадлежит s.subchain тогда и только тогда, когда a ∈ s.

LaTeX

$$$ [a] \\in s.\\mathrm{subchain} \\iff a \\in s. $$$

Lean4

@[simp]
theorem singleton_mem_subchain_iff : [a] ∈ s.subchain ↔ a ∈ s := by simp [cons_mem_subchain_iff]

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

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

Разделы

Аффилиация

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