English
If U and V are basis sets, there exists a basis set z contained in U ∩ V.
Русский
Если U и V — базисные множества, существует z ∈ p.basisSets, такой что z ⊆ U ∩ V.
LaTeX
$$∃ z ∈ p.basisSets, z ⊆ U ∩ V$$
Lean4
theorem basisSets_intersect (U V : Set E) (hU : U ∈ p.basisSets) (hV : V ∈ p.basisSets) :
∃ z ∈ p.basisSets, z ⊆ U ∩ V := by
classical
rcases p.basisSets_iff.mp hU with ⟨s, r₁, hr₁, hU⟩
rcases p.basisSets_iff.mp hV with ⟨t, r₂, hr₂, hV⟩
use ((s ∪ t).sup p).ball 0 (min r₁ r₂)
refine ⟨p.basisSets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), ?_⟩
rw [hU, hV, ball_finset_sup_eq_iInter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩), ball_finset_sup_eq_iInter _ _ _ hr₁,
ball_finset_sup_eq_iInter _ _ _ hr₂]
exact
Set.subset_inter (Set.iInter₂_mono' fun i hi => ⟨i, Finset.subset_union_left hi, ball_mono <| min_le_left _ _⟩)
(Set.iInter₂_mono' fun i hi => ⟨i, Finset.subset_union_right hi, ball_mono <| min_le_right _ _⟩)
