range_extend_subset — Mathlib

English

The range of the extend map is contained in the union of the range of g and the image of the complement (range f)ᶜ under g'.

Русский

Область значений отображения extend лежит в объединении диапазона g и образа g' над дополнением (range f)ᶜ.

LaTeX

$$$\\operatorname{range}(\\operatorname{extend} f g g') \\subseteq \\operatorname{range} g \\cup g'\\'\\big(\\operatorname{range} f\\big)^{c}$$$

Lean4

theorem range_extend_subset (f : α → β) (g : α → γ) (g' : β → γ) : range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ :=
  by
  classical
  rintro _ ⟨y, rfl⟩
  rw [extend_def]
  split_ifs with h
  exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]

Похожие утверждения