English
The infimum of pi f and principal(univ.pi s) equals bottom iff there exists an index i with f i ∧ principal(s i) = bottom.
Русский
Понижение pi f и principal(univ.pi s) достигают нуля тогда, когда существует i с f i ∧ principal(s i) = bottom.
LaTeX
$$$\pi f \sqcap \mathfrak{P}(\mathrm{Set.pi}(\mathrm{univ}, s)) = \bot \iff \exists i, f_i \sqcap \mathfrak{P}(s_i) = \bot$$$
Lean4
@[simp]
theorem pi_inf_principal_univ_pi_eq_bot : pi f ⊓ 𝓟 (Set.pi univ s) = ⊥ ↔ ∃ i, f i ⊓ 𝓟 (s i) = ⊥ :=
by
constructor
· simp only [inf_principal_eq_bot, mem_pi]
contrapose!
rintro (hsf : ∀ i, ∃ᶠ x in f i, x ∈ s i) I - t htf hts
have : ∀ i, (s i ∩ t i).Nonempty := fun i => ((hsf i).and_eventually (htf i)).exists
choose x hxs hxt using this
exact hts (fun i _ => hxt i) (mem_univ_pi.2 hxs)
· simp only [inf_principal_eq_bot]
rintro ⟨i, hi⟩
filter_upwards [mem_pi_of_mem i hi] with x using mt fun h => h i trivial
