isLUB_iff_of_subset_of_subset_closure

English

If s ⊆ t ⊆ closure s in a setting with ClosedIicTopology, then IsLUB s x ↔ IsLUB t x for any x.

Русский

Если s ⊆ t ⊆ closure s при заданной топологии, то IsLUB s x ↔ IsLUB t x для любого x.

LaTeX

$$$s \\subseteq t \\subseteq \\overline{s} \\Rightarrow IsLUB s x \\iff IsLUB t x$$$

Lean4

theorem isLUB_iff_of_subset_of_subset_closure {α : Type*} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α]
    {s t : Set α} (hst : s ⊆ t) (hts : t ⊆ closure s) {x : α} : IsLUB s x ↔ IsLUB t x :=
  isLUB_congr <| (upperBounds_closure (s := s) ▸ upperBounds_mono_set hts).antisymm <| upperBounds_mono_set hst

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