Relation_Induced_by_Mapping_is_Equivalence_Relation

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

equivalence-relationsmapping-theoryproofwiki

Let $f: S \to T$ be a mapping. Let $\RR_f \subseteq S \times S$ be the relation induced by $f$ $\tuple {s_1, s_2} \in \RR_f \iff \map f {s_1} = \map f {s_2}$ Then $\RR_f$ is an equivalence relation.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Relation_Induced_by_Mapping_is_Equivalence_Relation {S T : Type _} (f : S -> T) : Equivalence (fun s1 s2 : S => f s1 = f s2) := by sorry

Source

https://proofwiki.org/wiki/Relation_Induced_by_Mapping_is_Equivalence_Relation

View graph