ne_iff — Mathlib

English

Two functions f1,f2 are unequal iff there exists an argument a with f1(a) ≠ f2(a).

Русский

Разные функции f1 и f2 существуют, если существует аргумент a, для которого f1(a) ≠ f2(a).

LaTeX

$$$$ f_1 \\neq f_2 \\ \\Longleftrightarrow \\ \\\\exists a, f_1 a \\neq f_2 a. $$$$

Lean4

theorem ne_iff {β : α → Sort*} {f₁ f₂ : ∀ a, β a} : f₁ ≠ f₂ ↔ ∃ a, f₁ a ≠ f₂ a :=
  funext_iff.not.trans not_forall

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