English
Characterization of membership in a biInf of principal filters: t ∈ ⨅ (i : ι) (p i), 𝓟 (s i) iff there exists a finite I ⊆ ι with (∀ i ∈ I, p i) and ⋂ i∈I s_i ⊆ t.
Русский
Характеризация принадлежности t к биInf главных фильтров: t ∈ ⨅ (i) (p i), 𝓟 (s i) эквивалентно существованию конечного I ⊆ ι с условием (∀ i ∈ I, p i) и ⋂ i∈I s_i ⊆ t.
LaTeX
$$$ t \in \iInf (i : ι) (p i) \; \mathcal{P}(s i) \iff \exists I : Set ι, I.Finite \land (\forall i \in I, p i) \land \bigcap_{i \in I} s_i \subseteq t $$
Lean4
theorem mem_biInf_principal {ι : Type*} {p : ι → Prop} {s : ι → Set α} {t : Set α} :
t ∈ ⨅ (i : ι) (_ : p i), 𝓟 (s i) ↔ ∃ I : Set ι, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t :=
by
constructor
· simp only [mem_iInf (ι := ι), mem_iInf_of_finite, mem_principal]
rintro ⟨I, hIf, V, hV₁, hV₂, rfl⟩
choose! t ht₁ ht₂ using hV₁
refine ⟨I ∩ {i | p i}, hIf.inter_of_left _, fun i ↦ And.right, ?_⟩
simp only [mem_inter_iff, iInter_and, biInter_eq_iInter, ht₂, mem_setOf_eq]
gcongr with i hpi
exact ht₁ i hpi
· rintro ⟨I, hIf, hpI, hst⟩
rw [biInter_eq_iInter] at hst
refine mem_iInf_of_iInter hIf (fun i ↦ ?_) hst
simp [hpI i i.2]
