le_csInf_inter — Mathlib

English

The infima satisfy: sInf s ⊔ sInf t ≤ sInf(s ∩ t), if s and t are bounded below and their intersection is nonempty.

Русский

Инфимумы удовлетворяют: sInf s ⊔ sInf t ≤ sInf(s ∩ t), если множества ограничены снизу и пересечение непусто.

LaTeX

$$$\forall s,t:\\text{Set }\alpha,\ BddBelow\ s \\to BddBelow\ t \\to (s \cap t).Nonempty \\to sInf s \sqcup sInf t \le sInf(s\cap t)$$$

Lean4

/-- The infimum of an intersection of two sets is bounded below by the maximum of the
infima of each set, if all sets are bounded below and nonempty. -/
theorem le_csInf_inter : BddBelow s → BddBelow t → (s ∩ t).Nonempty → sInf s ⊔ sInf t ≤ sInf (s ∩ t) :=
  csSup_inter_le (α := αᵒᵈ)

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