sInf_eq_of_forall_ge_of_forall_gt_exists_lt

English

Let s ⊆ α and b ∈ α. If ∀ a ∈ s, b ≤ a and ∀ w > b there exists a ∈ s with a < w, then sInf s = b.

Русский

Пусть s ⊆ α и b ∈ α. Если ∀ a ∈ s, b ≤ a и ∀ w > b существует a ∈ s с a < w, то sInf s = b.

LaTeX

$$$$ \Big( \forall a \in s,\ b \le a \Big) \rightarrow \Big( \forall w,\ b < w \rightarrow \exists a \in s,\ a < w \Big) \rightarrow \operatorname{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 `csInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in conditionally complete
lattices. -/
theorem sInf_eq_of_forall_ge_of_forall_gt_exists_lt : (∀ a ∈ s, b ≤ a) → (∀ w, b < w → ∃ a ∈ s, a < w) → sInf s = b :=
  @sSup_eq_of_forall_le_of_forall_lt_exists_gt αᵒᵈ _ _ _

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