English
The module filter basis filter equals the infimum over i of the comaps along p_i of nhds 0.
Русский
База фильтра модуля равна инфимума по i из сопряжённых отображений p_i от 0-окрестностей.
LaTeX
$$p.moduleFilterBasis.toFilterBasis.filter = ⨅ i, (𝓝 0).comap (p i)$$
Lean4
theorem filter_eq_iInf (p : SeminormFamily 𝕜 F ι) : p.moduleFilterBasis.toFilterBasis.filter = ⨅ i, (𝓝 0).comap (p i) :=
by
refine le_antisymm (le_iInf fun i => ?_) ?_
· rw [p.moduleFilterBasis.toFilterBasis.hasBasis.le_basis_iff (Metric.nhds_basis_ball.comap _)]
intro ε hε
refine ⟨(p i).ball 0 ε, ?_, ?_⟩
· rw [← (Finset.sup_singleton : _ = p i)]
exact p.basisSets_mem { i } hε
· rw [id, (p i).ball_zero_eq_preimage_ball]
· rw [p.moduleFilterBasis.toFilterBasis.hasBasis.ge_iff]
rintro U (hU : U ∈ p.basisSets)
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, rfl⟩
rw [id, Seminorm.ball_finset_sup_eq_iInter _ _ _ hr, s.iInter_mem_sets]
exact fun i _ =>
Filter.mem_iInf_of_mem i
⟨Metric.ball 0 r, Metric.ball_mem_nhds 0 hr, Eq.subset (p i).ball_zero_eq_preimage_ball.symm⟩
