continuous_inclusion — Mathlib

English

If 𝓕 ≤ 𝓖, the inclusion of the restricted product corresponding to 𝓕 into the one corresponding to 𝓖 is continuous.

Русский

Если 𝓕 ≤ 𝓖, то включение ограниченного произведения в другое непрерывно.

LaTeX

$$$\\text{inclusion}_{R,A,h} : \\langle \\dots \\rangle \\to \\langle \\dots \\rangle$ is continuous whenever 𝓕 ≤ 𝓖.$$

Lean4

@[fun_prop]
theorem continuous_inclusion {𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖) : Continuous (inclusion R A h) :=
  by
  simp_rw [continuous_iff_coinduced_le, topologicalSpace, coinduced_iSup, coinduced_compose]
  exact iSup₂_le fun S hS ↦ le_iSup₂_of_le S (le_trans h hS) le_rfl

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