mono — Mathlib

English

If t ≤ u are topologies on S and a has evaluation in t, then a has evaluation in u.

Русский

Если t ≤ u для топологий на S и у a естьEvaluation в t, то он имеет Evaluation в u.

LaTeX

$$$t \\le u \\Rightarrow \\mathrm{HasEval}\\ _a^t \\Rightarrow \\mathrm{HasEval}\\ _a^u$$$

Lean4

theorem mono {S : Type*} [CommRing S] {a : σ → S} {t u : TopologicalSpace S} (h : t ≤ u) (ha : @HasEval _ _ _ t a) :
    @HasEval _ _ _ u a :=
  ⟨fun s ↦ Filter.Tendsto.mono_right (@HasEval.hpow _ _ _ t a ha s) (nhds_mono h),
    Filter.Tendsto.mono_right (@HasEval.tendsto_zero σ _ _ t a ha) (nhds_mono h)⟩

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