Ici_eq

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#IsCoatom.Ici_eq

English

If a is a coatom, then the up-set {x | a ≤ x} consists exactly of ⊤ and a.

Русский

Если a — коатом, то множество {x | a ≤ x} состоит ровно из ⊤ и a.

LaTeX

$$$ \\mathrm{IsCoatom}(a) \\rightarrow \\mathrm{SetIci}(a) = \\{\\top, a\\}. $$$

Lean4

theorem Ici_eq (h : IsCoatom a) : Set.Ici a = {⊤, a} :=
  h.dual.Iic_eq

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

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

Разделы

Аффилиация

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