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, then sSup s = sSup t.
Русский
Если каждый элемент s ограничен сверху элементом из t и каждый элемент t ограничен сверху элементом из s, тогда sSup s = sSup t.
LaTeX
$$$ (\forall x \in s, \exists y \in t, x \le y) \land (\forall y \in t, \exists x \in s, y \le x) \Rightarrow sSup s = sSup 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 supremum. This holds even when the sets may be empty or unbounded. -/
theorem csSup_eq_csSup_of_forall_exists_le {s t : Set α} (hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) (ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x) :
sSup s = sSup t := by
rcases eq_empty_or_nonempty s with rfl | s_ne
· have : t = ∅ := eq_empty_of_forall_notMem (fun y yt ↦ by simpa using ht y yt)
rw [this]
rcases eq_empty_or_nonempty t with rfl | t_ne
· have : s = ∅ := eq_empty_of_forall_notMem (fun x xs ↦ by simpa using hs x xs)
rw [this]
by_cases B : BddAbove s ∨ BddAbove t
· have Bs : BddAbove s := by
rcases B with hB | ⟨b, hb⟩
· exact hB
· refine ⟨b, fun x hx ↦ ?_⟩
rcases hs x hx with ⟨y, hy, hxy⟩
exact hxy.trans (hb hy)
have Bt : BddAbove t := by
rcases B with ⟨b, hb⟩ | hB
· refine ⟨b, fun y hy ↦ ?_⟩
rcases ht y hy with ⟨x, hx, hyx⟩
exact hyx.trans (hb hx)
· exact hB
apply le_antisymm
· apply csSup_le s_ne (fun x hx ↦ ?_)
rcases hs x hx with ⟨y, yt, hxy⟩
exact hxy.trans (le_csSup Bt yt)
· apply csSup_le t_ne (fun y hy ↦ ?_)
rcases ht y hy with ⟨x, xs, hyx⟩
exact hyx.trans (le_csSup Bs xs)
· simp [csSup_of_not_bddAbove, (not_or.1 B).1, (not_or.1 B).2]
