le_pi_principal — Mathlib

English

The principal filter on the product of all sets univ pi s is below the Pi-filter of principal(s i).

Русский

Принципиальный фильтр на произведение имеет отношение к нижнему пределу Pi-фильтра на главных цилиндрах.

LaTeX

$$$\mathfrak{P}(\mathrm{univ}.\pi s) \le \pi (\mathfrak{P}(s_i))$$$

Lean4

theorem le_pi_principal (s : (i : ι) → Set (α i)) : 𝓟 (univ.pi s) ≤ pi fun i ↦ 𝓟 (s i) :=
  le_pi.2 fun i ↦ tendsto_principal_principal.2 fun _f hf ↦ hf i trivial

Похожие утверждения