csInf_eq_csInf_of_forall_exists_le

English

If every element of s is bounded above by some element of t, and every element of t is bounded above by some element of s (dual form), then sInf s = sInf t.

Русский

Если каждый элемент s ограничен сверху элементом из t, и каждый элемент t ограничен сверху элементом из s (двойной вид), то sInf s = sInf t.

LaTeX

$$$ (\forall x \in s, \exists y \in t, y \le x) \land (\forall y \in t, \exists x \in s, x \le y) \Rightarrow sInf s = sInf t $$$

Lean4

/-- When every element of a set `s` is bounded by an element of a set `t`, and conversely, then
`s` and `t` have the same infimum. This holds even when the sets may be empty or unbounded. -/
theorem csInf_eq_csInf_of_forall_exists_le {s t : Set α} (hs : ∀ x ∈ s, ∃ y ∈ t, y ≤ x) (ht : ∀ y ∈ t, ∃ x ∈ s, x ≤ y) :
    sInf s = sInf t :=
  csSup_eq_csSup_of_forall_exists_le (α := αᵒᵈ) hs ht

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