Theorems · Theorem · order theory

csInf_eq_iff

∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α],
  s.Nonempty → ∀ (n : α), sInf s = n ↔ n ∈ s ∧ ∀ a ∈ s, n ≤ a

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Basic

Cited by

0 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ConditionallyCompleteLinearOrderWellFoundedLT