comp_rangeSplitting — Mathlib

English

For every f: A→B and g: range(f) → A given by rangeSplitting, f ∘ rangeSplitting(f) = Subtype.val on range(f).

Русский

Для каждого отображения f: A→B и соответствующего rangeSplitting, выполнено f ∘ rangeSplitting(f) = Subtype.val на range(f).

LaTeX

$$$$f \\circ \\mathrm{rangeSplitting}(f) = \\mathrm{Subtype.val}$$$$

Lean4

@[simp]
theorem comp_rangeSplitting (f : α → β) : f ∘ rangeSplitting f = Subtype.val :=
  by
  ext
  simp only [Function.comp_apply]
  apply apply_rangeSplitting

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