eval_continuous — Mathlib

English

For each fixed y ∈ F, the evaluation map x ↦ B(x,y) is continuous; more generally, the map x ↦ B(x,·) is continuous as a map into F → 𝕜.

Русский

Для каждого фиксированного y ∈ F отображение оценки x ↦ B(x,y) непрерывно; в общем виде отображение x ↦ B(x,·) непрерывно как мапа в F → 𝕜.

LaTeX

$$theorem eval_continuous (y : F) : Continuous fun x : WeakBilin B => B x y$$

Lean4

@[fun_prop]
theorem eval_continuous (y : F) : Continuous fun x : WeakBilin B => B x y :=
  (continuous_pi_iff.mp (coeFn_continuous B)) y

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