isGLB_inter_iff — Mathlib

English

If s is dense and t is open, IsGLB(t ∩ s) x is equivalent to IsGLB t x.

Русский

Если s плотное и t открытое, IsGLB(t ∩ s) x эквивалентно IsGLB t x.

LaTeX

$$Dense s → IsOpen t → IsGLB(t ∩ s) x ↔ IsGLB t x$$

Lean4

theorem isGLB_inter_iff {α : Type*} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {s t : Set α} (hs : Dense s)
    (ht : IsOpen t) {x : α} : IsGLB (t ∩ s) x ↔ IsGLB t x :=
  hs.isLUB_inter_iff (α := αᵒᵈ) ht

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