English
A variant of the iInf representation: U ∈ ⨅ i s_i if and only if there exists a finite index set I and V_i ∈ s_i for i ∈ I with U = ⋂ i∈I V_i.
Русский
Вариант представления iInf: U ∈ ⨅ i s_i тогда и только тогда, существует конечное множество индексов I и V_i ∈ s_i для i ∈ I, так что U = ⋂_{i∈I} V_i.
LaTeX
$$$ (U \in \iInf_i s_i) \iff \exists I : Finite, \exists V : I \to Set α, (\forall i:I, V_i \in s_i) \land U = \bigcap_{i\in I} V_i $$
Lean4
theorem mem_iInf' {ι} {s : ι → Filter α} {U : Set α} :
(U ∈ ⨅ i, s i) ↔
∃ I : Set ι,
I.Finite ∧ ∃ V : ι → Set α, (∀ i, V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ (U = ⋂ i ∈ I, V i) ∧ U = ⋂ i, V i :=
by
classical
simp only [mem_iInf, biInter_eq_iInter]
refine ⟨?_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩
rintro ⟨I, If, V, hV, rfl⟩
refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
· dsimp only
split_ifs
exacts [hV ⟨i, _⟩, univ_mem]
· exact dif_neg hi
·
simp only [iInter_dite, biInter_eq_iInter, dif_pos (Subtype.coe_prop _), Subtype.coe_eta, iInter_univ, inter_univ,
true_and]
