English
The intersection of bases of two topologies forms a basis for their infimum topology.
Русский
Пересечение двух баз топологий образует базис для наибольшей общности этих топологий.
LaTeX
$$$\\text{IsTopologicalBasis}(t_1, B_1) \\land \\text{IsTopologicalBasis}(t_2, B_2) \\Rightarrow \\text{IsTopologicalBasis}(t_1 \\cap t_2, \\mathrm{image2}(\\cdot \\cap \\cdot)\\; B_1\\; B_2)$$$
Lean4
protected theorem inf {t₁ t₂ : TopologicalSpace β} {B₁ B₂ : Set (Set β)} (h₁ : IsTopologicalBasis (t := t₁) B₁)
(h₂ : IsTopologicalBasis (t := t₂) B₂) : IsTopologicalBasis (t := t₁ ⊓ t₂) (image2 (· ∩ ·) B₁ B₂) :=
by
refine .of_hasBasis_nhds (t := ?_) fun a ↦ ?_
rw [nhds_inf (t₁ := t₁)]
convert ((h₁.nhds_hasBasis (t := t₁)).inf (h₂.nhds_hasBasis (t := t₂))).to_image_id
aesop
