range_subset_range_iff_exists_comp

English

range f ⊆ range g iff ∃ h: α → β with f = g ∘ h.

Русский

range f ⊆ range g эквивалентно существованию h: α → β such that f = g ∘ h.

LaTeX

$$$ \\operatorname{range} f \\subseteq \\operatorname{range} g\\;\\iff\\; \\exists h: \\alpha \\to \\beta,\\ f = g \\circ h$$$

Lean4

theorem range_subset_range_iff_exists_comp {f : α → γ} {g : β → γ} : range f ⊆ range g ↔ ∃ h : α → β, f = g ∘ h := by
  simp only [range_subset_iff, mem_range, Classical.skolem, funext_iff, (· ∘ ·), eq_comm]

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