instSemilatticeInf

Mathlib.Topology.Sets.Compacts

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.CompactOpens.instSemilatticeInf

English

CompactOpens α carries a SemilatticeInf structure with inf given by the coe_inf construction.

Русский

CompactOpens α имеет структуру полубопорядка Inf, где Inf задается через coe_inf.

LaTeX

$$$\text{SemilatticeInf} (CompactOpens α)$$$

Lean4

instance instSemilatticeInf : SemilatticeInf (CompactOpens α) :=
  SetLike.coe_injective.semilatticeInf _ coe_inf

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

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

Разделы

Аффилиация

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