infClosed

Mathlib.Order.SupClosed

URI: https://scilib.ai/kg/mathlib#LinearOrder.infClosed

English

Range of a lattice hom is a Sublattice (repeat variant).

Русский

Образ гомоморфизма решетки является субрешеткой (повтор):

LaTeX

$$IsSublattice (Set.range f)$$

Lean4

@[simp]
protected theorem infClosed (s : Set α) : InfClosed s := fun a ha b hb ↦ by cases le_total a b <;> simp [*]

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

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

Разделы

Аффилиация

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