Condition_for_Composite_Mapping_on_Left

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result Condition_for_Composite_Mapping_on_Left is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

There exists a mapping h: B -> C such that g = h circ f iff for all x,y in A, f(x) = f(y) implies g(x) = g(y).

Why this node was retired

The posted statement is

import Mathlib.Analysis.Complex.Basic

theorem Condition_for_Composite_Mapping_on_Left
  {A B C : Type _} [Nonempty C] (f : A -> B) (g : A -> C) :
  (forall x y : A, f x = f y -> g x = g y) -> True := by sorry

The goal is an implication whose conclusion is True, so it is closed by fun _ => trivial. The antecedent ∀ x y, f x = f y → g x = g y is never used, and the composite mapping the name refers to is never constructed.

What a faithful statement would require

The conclusion must assert the existence of h : B → C with h ∘ f = g, rather than True.

No corrected replacement node exists yet.