lt_csInf_iff — Mathlib

English

For a finite set s, a < sInf s iff each x ∈ s satisfies a < x.

Русский

Для конечного множества s, a < sInf s тогда и только тогда, когда для каждого x ∈ s верно a < x.

LaTeX

$$$(hs : s.Finite) (h : s.Nonempty) : a < sInf s \Leftrightarrow \forall x ∈ s, a < x$$$

Lean4

theorem lt_csInf_iff (hs : s.Finite) (h : s.Nonempty) : a < sInf s ↔ ∀ x ∈ s, a < x :=
  @Set.Finite.csSup_lt_iff αᵒᵈ _ _ _ hs h

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