of_isCoatom_coe_Ici

Mathlib.Order.Atoms

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

English

If a is a coatom of the interval Set.Ici x, then its underlying element a.val is a coatom in α.

Русский

Если a является коатомом интервала Set.Ici x, то его прообраз в α, a.val, является коатомом в α.

LaTeX

$$IsCoatom a → IsCoatom (a : α)$$

Lean4

theorem of_isCoatom_coe_Ici {a : Set.Ici x} (ha : IsCoatom a) : IsCoatom (a : α) :=
  @IsAtom.of_isAtom_coe_Iic αᵒᵈ _ _ x a ha

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

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

Разделы

Аффилиация

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