Condition_for_Composite_Mapping_on_Right

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result Condition_for_Composite_Mapping_on_Right 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: C -> B such that g = f circ h iff Im(g) is a subset of Im(f).

Why this node was retired

The posted statement is

import Mathlib.Analysis.Complex.Basic

theorem Condition_for_Composite_Mapping_on_Right
  {A B C : Type _} (f : B -> A) (g : C -> A) :
  (Set.range g <= Set.range f) -> True := by sorry

The goal is an implication whose conclusion is True, so it is closed by fun _ => trivial. The antecedent Set.range g ≤ Set.range f is never used, and no composite mapping is produced.

What a faithful statement would require

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

No corrected replacement node exists yet.