interior_inter — Mathlib

English

The interior distributes over intersection: int(s ∩ t) = int(s) ∩ int(t).

Русский

Интерьер распределяется по пересечению: int(s ∩ t) = int(s) ∩ int(t).

LaTeX

$$$ \operatorname{int}(s \cap t) = \operatorname{int}(s) \cap \operatorname{int}(t)$$$

Lean4

@[simp]
theorem interior_inter : interior (s ∩ t) = interior s ∩ interior t :=
  (Monotone.map_inf_le (fun _ _ ↦ interior_mono) s t).antisymm <|
    interior_maximal (inter_subset_inter interior_subset interior_subset) <| isOpen_interior.inter isOpen_interior

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