English
The range of the extend map equals the union of the range of g and the image of the complement of range f under g, provided f is injective.
Русский
Диапазон extend равен объединению диапазона g и образа g' над дополнением range f, при условии инъективности f.
LaTeX
$$$\\operatorname{range}(\\operatorname{extend} f g g') = \\operatorname{range} g \\cup g'\\big(\\operatorname{range} f\\big)^{c}$$$
Lean4
theorem range_extend {f : α → β} (hf : Injective f) (g : α → γ) (g' : β → γ) :
range (extend f g g') = range g ∪ g' '' (range f)ᶜ :=
by
refine (range_extend_subset _ _ _).antisymm ?_
rintro z (⟨x, rfl⟩ | ⟨y, hy, rfl⟩)
exacts [⟨f x, hf.extend_apply _ _ _⟩, ⟨y, extend_apply' _ _ _ hy⟩]
