English
Let I be a finite index set and s_i be a family of sets with V_i ∈ s_i for each i ∈ I. If ⋂_{i ∈ I} V_i ⊆ U, then U belongs to the infimum filter ⨅ i, s_i.
Русский
Пусть I — конечное множество индексов и для каждого i ∈ I имеется множество V_i ∈ s_i. Если ⋂_{i ∈ I} V_i ⊆ U, то U принадлежит инфимууму фильтров ⨅ i, s_i.
LaTeX
$$$ I \text{ finite} \to U \in \bigwedge_{i} s_i \quad\text{from}\quad (\forall i\in I, V_i \in s_i) \land (\bigcap_{i\in I} V_i \subseteq U) \Rightarrow U \in \bigwedge_i s_i $$
Lean4
theorem mem_iInf_of_iInter {ι} {s : ι → Filter α} {U : Set α} {I : Set ι} (I_fin : I.Finite) {V : I → Set α}
(hV : ∀ (i : I), V i ∈ s i) (hU : ⋂ i, V i ⊆ U) : U ∈ ⨅ i, s i :=
by
haveI := I_fin.fintype
refine mem_of_superset (iInter_mem.2 fun i => ?_) hU
exact mem_iInf_of_mem (i : ι) (hV _)
