English
The infimum of the union equals the meet of the infima: sInf(s ∪ t) = sInf s ⊓ sInf t, provided s and t are nonempty and bounded below.
Русский
Infimum объединения равен их наименьшему пределу: sInf(s ∪ t) = sInf s ⊓ sInf t, при условии, что s и t непусты и ограничены снизу.
LaTeX
$$$\forall s,t:\\text{Set }\alpha,\ BddBelow\ s → BddBelow\ t \\to s.Nonempty \\to t.Nonempty \\to sInf(s\cup t) = sInf s \sqcap sInf t$$$
Lean4
/-- The `sInf` of a union of two sets is the min of the infima of each subset, under the assumptions
that all sets are bounded below and nonempty. -/
theorem csInf_union (hs : BddBelow s) (sne : s.Nonempty) (ht : BddBelow t) (tne : t.Nonempty) :
sInf (s ∪ t) = sInf s ⊓ sInf t :=
csSup_union (α := αᵒᵈ) hs sne ht tne
