inter_of_isOpen_left — Mathlib

English

If s is dense, t is dense, and s is open, then s ∩ t is dense.

Русский

Если s плотное, t плотное, и s открыто, то s ∩ t плотное.

LaTeX

$$$\\text{Dense}(s \\cap t)$$$

Lean4

/-- The intersection of an open dense set with a dense set is a dense set. -/
theorem inter_of_isOpen_left (hs : Dense s) (ht : Dense t) (hso : IsOpen s) : Dense (s ∩ t) := fun x =>
  closure_minimal hso.inter_closure isClosed_closure <| by simp [hs.closure_eq, ht.closure_eq]

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