map_pos_of_ne_one

Mathlib.Algebra.Order.Hom.Basic

URI: https://scilib.ai/kg/mathlib#map_pos_of_ne_one

← MathLib Explorer

English

If x ≠ 1 in a suitable group, then f x > 0.

Русский

Если x ≠ 1 в подходящей группе, то f x > 0.

LaTeX

$$$x \neq 1 \Rightarrow 0 < f(x)$$$

Lean4

@[to_additive]
theorem map_pos_of_ne_one [Group α] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [GroupNormClass F α β]
    (f : F) {x : α} (hx : x ≠ 1) : 0 < f x :=
  (apply_nonneg _ _).lt_of_ne <| ((map_ne_zero_iff_ne_one _).2 hx).symm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru