English
The infimum of two HasBasis families corresponds to taking pair indices and intersections of the corresponding sets.
Русский
Наименьшее среди двух базисов задается парами индексов и пересечениями соответствующих множеств.
LaTeX
$$inf' (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') : (l ⊓ l').HasBasis (fun i : PProd ι ι' => p i.1 ∧ p' i.2) fun i => s i.1 ∩ s' i.2$$
Lean4
theorem inf' (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
(l ⊓ l').HasBasis (fun i : PProd ι ι' => p i.1 ∧ p' i.2) fun i => s i.1 ∩ s' i.2 :=
⟨by
intro t
constructor
· simp only [mem_inf_iff, hl.mem_iff, hl'.mem_iff]
rintro ⟨t, ⟨i, hi, ht⟩, t', ⟨i', hi', ht'⟩, rfl⟩
exact ⟨⟨i, i'⟩, ⟨hi, hi'⟩, inter_subset_inter ht ht'⟩
· rintro ⟨⟨i, i'⟩, ⟨hi, hi'⟩, H⟩
exact mem_inf_of_inter (hl.mem_of_mem hi) (hl'.mem_of_mem hi') H⟩
