Ici

Mathlib.Order.Atoms

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

English

If a is a coatom and x ≤ a, then the element ⟨a, x ≤ a⟩ in the set Ici x is a coatom.

Русский

Если a — коатом и x ≤ a, то элемент ⟨a, x ≤ a⟩ в множесте Set.Ici x является коатомом.

LaTeX

$$IsCoatom a → ∀ hax : x ≤ a, IsCoatom ⟨a, hax⟩$$

Lean4

theorem Ici (ha : IsCoatom a) (hax : x ≤ a) : IsCoatom (⟨a, hax⟩ : Set.Ici x) :=
  ha.dual.Iic hax

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

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

Разделы

Аффилиация

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