isGLB_iff_of_subset_of_subset_closure

English

If s ⊆ t ⊆ closure s with ClosedIciTopology, then IsGLB s x ↔ IsGLB t x for any x.

Русский

Если s ⊆ t ⊆ closure s при ClosedIciTopology, то IsGLB s x ⇔ IsGLB t x.

LaTeX

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

Lean4

theorem isGLB_iff_of_subset_of_subset_closure {α : Type*} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α]
    {s t : Set α} (hst : s ⊆ t) (hts : t ⊆ closure s) {x : α} : IsGLB s x ↔ IsGLB t x :=
  isLUB_iff_of_subset_of_subset_closure (α := αᵒᵈ) hst hts

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