le_einfsep_pi_of_le — Mathlib

English

Analogous to the previous, for a product-type setting, if for all i, c ≤ einfsep(s(i)), then c ≤ einfsep(Set.pi univ s).

Русский

Аналогично, в произведении: если для каждого i выполняется c ≤ einfsep(s(i)), то c ≤ einfsep(Set.pi univ s).

LaTeX

$$$ \forall i, c \le (s(i)).einfsep \Rightarrow c \le \operatorname{einfsep}(\mathrm{Set.pi}\;\mathrm{univ}\; s) $$$

Lean4

theorem le_einfsep_pi_of_le {X : β → Type*} [Fintype β] [∀ b, PseudoEMetricSpace (X b)] {s : ∀ b : β, Set (X b)}
    {c : ℝ≥0∞} (h : ∀ b, c ≤ einfsep (s b)) : c ≤ einfsep (Set.pi univ s) :=
  by
  refine le_einfsep fun x hx y hy hxy => ?_
  rw [mem_univ_pi] at hx hy
  rcases Function.ne_iff.mp hxy with ⟨i, hi⟩
  exact le_trans (le_einfsep_iff.1 (h i) _ (hx _) _ (hy _) hi) (edist_le_pi_edist _ _ i)

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