neLocus_eq_empty — Mathlib

English

The difference locus of f and g is empty if and only if f and g are equal.

Русский

Локус различий между f и g равен пустому множеству тогда и только тогда, когда f = g.

LaTeX

$$$ f \neLocus g = \emptyset \iff f = g $$$

Lean4

@[simp]
theorem neLocus_eq_empty {f g : Π₀ a, N a} : f.neLocus g = ∅ ↔ f = g :=
  ⟨fun h ↦ ext fun a ↦ not_not.mp (mem_neLocus.not.mp (Finset.eq_empty_iff_forall_notMem.mp h a)), fun h ↦
    h ▸ by simp only [neLocus, Ne, not_true, Finset.filter_false]⟩

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