csInf_le_of_le — Mathlib

English

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

Русский

Пусть α — условно полноупорядоченная решетка. Пусть s ограничено снизу, непусто, и существует b ∈ s с b ≤ a. Тогда sInf(s) ≤ a.

LaTeX

$$$BddBelow(s) \land b \in s \land b \le a \rightarrow \mathrm{sInf}(s) \le a$$$

Lean4

theorem csInf_le_of_le (hs : BddBelow s) (hb : b ∈ s) (h : b ≤ a) : sInf s ≤ a :=
  le_trans (csInf_le hs hb) h

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