English
Characterization of membership in pi f by finite supports: s ∈ pi f iff there exists a finite I and t with t_i ∈ f_i for all i and I.pi t ⊆ s.
Русский
Характеризация членства в pi f через конечную опору: s ∈ pi f тогда существует конечный I и t с t_i ∈ f_i для всех i и I.pi t ⊆ s.
LaTeX
$$$s \in \pi f \iff \exists I, I.Finite \land \exists t : \forall i, Set(\alpha_i), (\forall i, t_i \in f_i) \land I.pi t \subseteq s$$$
Lean4
theorem mem_pi {s : Set (∀ i, α i)} :
s ∈ pi f ↔ ∃ I : Set ι, I.Finite ∧ ∃ t : ∀ i, Set (α i), (∀ i, t i ∈ f i) ∧ I.pi t ⊆ s :=
by
constructor
· simp only [pi, mem_iInf', mem_comap, pi_def]
rintro ⟨I, If, V, hVf, -, rfl, -⟩
choose t htf htV using hVf
exact ⟨I, If, t, htf, iInter₂_mono fun i _ => htV i⟩
· rintro ⟨I, If, t, htf, hts⟩
exact mem_of_superset (pi_mem_pi If fun i _ => htf i) hts
