isSublattice

Mathlib.Order.SupClosed

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

English

IsSublattice of preimage under toDual is equivalent to IsSublattice of the image.

Русский

IsSublattice прообраза под toDual эквивалентен IsSublattice образа.

LaTeX

$$IsSublattice (toDual^{-1}' s) ↔ IsSublattice s$$

Lean4

@[simp]
protected theorem isSublattice (s : Set α) : IsSublattice s :=
  ⟨LinearOrder.supClosed _, LinearOrder.infClosed _⟩

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

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

Разделы

Аффилиация

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