inf_sSup_le_iSup_inf — Mathlib

English

In a complete Boolean algebra, for any a and any set s, the infimum of {a ∧ b : b ∈ s} is ≤ a ∧ (inf s).

Русский

В полной булевой алгебре для любого a и множества s выполняется: \bigwedge_{b∈s}(a ∧ b) ≤ a ∧ (∧ s).

LaTeX

$$$\forall a, s,\; \bigwedge_{b \in s} (a \wedge b) \le a \wedge (\bigwedge s).$$$

Lean4

@[deprecated "use `inf_sSup_eq.le` instead" (since := "2025-06-15")]
theorem inf_sSup_le_iSup_inf (a : α) (s : Set α) : a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b :=
  gc_inf_himp.l_sSup.le

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