isLUB_inter_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isLUB_inter_iff {α : Type*} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s t : Set α} (hs : Dense s)
    (ht : IsOpen t) {x : α} : IsLUB (t ∩ s) x ↔ IsLUB t x :=
  isLUB_iff_of_subset_of_subset_closure (by simp) <| hs.open_subset_closure_inter ht

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