inter — Mathlib

English

If s and t are locally closed, then s ∩ t is locally closed.

Русский

Если s и t локально замкнуты, то их пересечение локально замкнуто.

LaTeX

$$$\text{IsLocallyClosed}(s) \wedge \text{IsLocallyClosed}(t) \Rightarrow \text{IsLocallyClosed}(s \cap t)$$$

Lean4

theorem inter (hs : IsLocallyClosed s) (ht : IsLocallyClosed t) : IsLocallyClosed (s ∩ t) :=
  by
  obtain ⟨U₁, Z₁, hU₁, hZ₁, rfl⟩ := hs
  obtain ⟨U₂, Z₂, hU₂, hZ₂, rfl⟩ := ht
  refine ⟨_, _, hU₁.inter hU₂, hZ₁.inter hZ₂, inter_inter_inter_comm U₁ Z₁ U₂ Z₂⟩

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