English
Let f and g be dependent finitely supported functions f,g : Π₀ a, N a. Then the set of indices where f and g differ is exactly the set { a : α | f(a) ≠ g(a) }. Equivalently, a is in the difference locus of f and g if and only if their values at a are not equal.
Русский
Пусть f и g — зависимые конечносupport функции f,g : Π₀ a, N a. Тогда множество индексов, на которых они различаются, равно { a ∈ α | f(a) ≠ g(a) }. Иными словами, принадлежность a к локусу различий эквивалентна неравенству значений в a.
LaTeX
$$$ a \in \{ x \in \alpha \mid f(x) \neq g(x) \} \iff f(a) \neq g(a) $$$
Lean4
@[simp]
theorem mem_neLocus {f g : Π₀ a, N a} {a : α} : a ∈ f.neLocus g ↔ f a ≠ g a := by
simpa only [neLocus, Finset.mem_filter, Finset.mem_union, mem_support_iff, and_iff_right_iff_imp] using Ne.ne_or_ne _
