csInf_le_csInf — Mathlib

English

Let α be a ConditionallyCompleteLattice. If s ⊆ t and s is nonempty with t bounded below, then sInf(t) ≤ sInf(s).

Русский

Пусть α — условно CompleteLattice. Пусть s ⊆ t, s непусто и t ограничено снизу. Тогда sInf(t) ≤ sInf(s).

LaTeX

$$$(t \text{ bounded below}) \land s \neq \varnothing \land (s \subseteq t) \rightarrow \mathrm{sInf}(t) \le \mathrm{sInf}(s)$$$

Lean4

@[gcongr low]
theorem csInf_le_csInf (ht : BddBelow t) (hs : s.Nonempty) (h : s ⊆ t) : sInf t ≤ sInf s :=
  le_csInf hs fun _ ha => csInf_le ht (h ha)

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