csInf_eq_of_forall_ge_of_forall_gt_exists_lt

English

A dual version: if s is nonempty, every a ∈ s is ≥ b, and every w > b has some a ∈ s with a < w, then sInf s = b.

Русский

Двойственная версия: если s непусто, каждый a ∈ s ≥ b, и для любого w > b существует a ∈ s такой, что a < w, тогда sInf s = b.

LaTeX

$$CsInf_eq_of_forall_ge_of_forall_gt_exists_lt : s.Nonempty → (∀ a ∈ s, b ≤ a) → (∀ w, b < w → ∃ a ∈ s, a < w) → sInf s = b$$

Lean4

/-- Introduction rule to prove that `b` is the infimum of `s`: it suffices to check that `b`
is smaller than all elements of `s`, and that this is not the case of any `w>b`.
See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/
theorem csInf_eq_of_forall_ge_of_forall_gt_exists_lt :
    s.Nonempty → (∀ a ∈ s, b ≤ a) → (∀ w, b < w → ∃ a ∈ s, a < w) → sInf s = b :=
  csSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ)

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