le_sInf_inter

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#le_sInf_inter

English

A dual form asserting the same inequality via dual order (order duality).

Русский

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

LaTeX

$$$$ \text{(duality form)} $$$$

Lean4

theorem le_sInf_inter {s t : Set α} : sInf s ⊔ sInf t ≤ sInf (s ∩ t) :=
  @sSup_inter_le αᵒᵈ _ _ _

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

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

Разделы

Аффилиация

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