ne_iff

Mathlib.Data.FunLike.Basic

URI: https://scilib.ai/kg/mathlib#DFunLike.ne_iff

English

Two function-like objects are unequal iff there exists an argument where they differ.

Русский

Два объекта F неравны тогда, когда существует аргумент a, при котором они различаются.

LaTeX

$$$f \neq g \iff \exists a, f(a) \neq g(a).$$$

Lean4

theorem ne_iff {f g : F} : f ≠ g ↔ ∃ a, f a ≠ g a :=
  ext_iff.not.trans not_forall

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

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

Разделы

Аффилиация

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