English
If s is in the infimum of the filters s_i, there exists a family V : I → Set α with V_i ∈ s_i for all i ∈ I such that s = ⋂ i ∈ I, V_i (and hence s = ⋂ i, V_i).
Русский
Если множество s принадлежит инфиминууму фильтров s_i, существуют множества V_i с V_i ∈ s_i для всех i ∈ I such что s = ⋂_{i∈I} V_i (и, по сути, s = ⋂_i V_i).
LaTeX
$$$ (U \in \bigwedge_i s_i) \iff \exists I\; (I \text{ finite}) \; \exists V:I \to Set\alpha,\; (\forall i:I, V_i \in s_i) \land U = \bigcap_{i} V_i $$
Lean4
theorem mem_iInf {ι} {s : ι → Filter α} {U : Set α} :
(U ∈ ⨅ i, s i) ↔ ∃ I : Set ι, I.Finite ∧ ∃ V : I → Set α, (∀ (i : I), V i ∈ s i) ∧ U = ⋂ i, V i :=
by
constructor
· rw [iInf_eq_generate, mem_generate_iff]
rintro ⟨t, tsub, tfin, tinter⟩
rcases eq_finite_iUnion_of_finite_subset_iUnion tfin tsub with ⟨I, Ifin, σ, σfin, σsub, rfl⟩
rw [sInter_iUnion] at tinter
set V := fun i => U ∪ ⋂₀ σ i with hV
have V_in : ∀ (i : I), V i ∈ s i := by
rintro i
have : ⋂₀ σ i ∈ s i := by
rw [sInter_mem (σfin _)]
apply σsub
exact mem_of_superset this subset_union_right
refine ⟨I, Ifin, V, V_in, ?_⟩
rwa [hV, ← union_iInter, union_eq_self_of_subset_right]
· rintro ⟨I, Ifin, V, V_in, rfl⟩
exact mem_iInf_of_iInter Ifin V_in Subset.rfl
