seminormFromConst_one — Mathlib

English

The value of seminormFromConst' hf1 hc hpm at 1 equals 1; i.e., seminormFromConst' hf1 hc hpm 1 = 1.

Русский

Значение на единице равно единице: seminormFromConst' hf1 hc hpm 1 = 1.

LaTeX

$$$\operatorname{seminormFromConst'} hf1 hc hpm 1 = 1$$$

Lean4

/-- `seminormFromConst' hf1 hc hpm 1 = 1`. -/
theorem seminormFromConst_one : seminormFromConst' hf1 hc hpm 1 = 1 :=
  by
  apply tendsto_nhds_unique_of_eventuallyEq (seminormFromConst_isLimit hf1 hc hpm 1) tendsto_const_nhds
  simp only [EventuallyEq, eventually_atTop, ge_iff_le]
  exact ⟨1, seminormFromConst_seq_one hc hpm⟩

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