Codomain_of_Composite_Relation
Provedcomposite-relationsproofwiki
The range of a composite function g ∘ f is a subset of the range of g: range(g ∘ f) ⊆ range(g)
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Function
Formal statement
theorem Codomain_of_Composite_Relation {α : Type _} {β : Type _} {γ : Type _} (f : α → β) (g : β → γ) : Set.range (g ∘ f) ⊆ Set.range g := by sorrySource