apply_eq_apply_of_inseparable — Mathlib

English

Let f be a (class of) additive-group homomorphism that vanishes on zero-norm elements. Then f sends inseparable pairs x, y to equal values: f x = f y.

Русский

Пусть f — некий гомоморфизм аддитивной группы, который обращает в ноль элементы нулевой нормы. Тогда для inseparable пар x, y выполняется f x = f y.

LaTeX

$$$ \\forall x,y,\\ Inseparable(x,y) \\Rightarrow f x = f y $$$

Lean4

theorem apply_eq_apply_of_inseparable {F : Type*} [FunLike F M N] [AddMonoidHomClass F M N] (f : F)
    (hf : ∀ x, ‖x‖ = 0 → f x = 0) : ∀ x y, Inseparable x y → f x = f y := fun x y h ↦
  eq_of_sub_eq_zero <| by
    rw [← map_sub]
    rw [Metric.inseparable_iff, dist_eq_norm] at h
    exact hf (x - y) h

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