closure_inter_open_nonempty_iff — Mathlib

English

Let t be open. Then (closure s ∩ t) Nonempty iff (s ∩ t) Nonempty.

Русский

Пусть t открыто. Тогда (closure s ∩ t) непусто тогда, когда (s ∩ t) непусто.

LaTeX

$$$\\\\IsOpen(t) \\\\Rightarrow ((\\\\overline{s} \\\\cap t).Nonempty \\\\iff (s \\\\cap t).Nonempty)$$$

Lean4

theorem closure_inter_open_nonempty_iff (h : IsOpen t) : (closure s ∩ t).Nonempty ↔ (s ∩ t).Nonempty :=
  ⟨fun ⟨_x, hxcs, hxt⟩ => inter_comm t s ▸ mem_closure_iff.1 hxcs t h hxt, fun h =>
    h.mono <| inf_le_inf_right t subset_closure⟩

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