notMem_neLocus — Mathlib

English

For f,g : Π₀ a, N a, an element a is not in the difference locus of f and g if and only if f(a) = g(a).

Русский

Для функций f,g: Π₀ a, N a: элемент a не принадлежит локусу различий f и g тогда и только тогда, когда f(a) = g(a).

LaTeX

$$$ a \notin \{ x \in \alpha \mid f(x) \neq g(x) \} \iff f(a) = g(a) $$$

Lean4

theorem notMem_neLocus {f g : Π₀ a, N a} {a : α} : a ∉ f.neLocus g ↔ f a = g a :=
  mem_neLocus.not.trans not_ne_iff

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