range_nontrivial

Mathlib.Algebra.GroupWithZero.Range

URI: https://scilib.ai/kg/mathlib#MonoidWithZeroHom.range_nontrivial

English

The set-theoretic range of f is nontrivial when the codomain is nontrivial.

Русский

Множество значений функции f не тривиально, если кодом является ненулевая структура.

LaTeX

$$Set.range f .Nontrivial$$

Lean4

theorem range_nontrivial : (Set.range f).Nontrivial :=
  Set.nontrivial_coe_sort.mp f.mrange_nontrivial

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

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

Разделы

Аффилиация

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