range_eq — Mathlib

English

If f : α ⊕ β → γ, then the range of f is the union of the ranges of f on α via inl and on β via inr.

Русский

Если f : α ⊕ β → γ, то образ f равен объединению образов f на α через inl и на β через inr.

LaTeX

$$$$ \\operatorname{range}(f) = \\operatorname{range}(f \\circ \\mathrm{Sum}.inl) \\cup \\operatorname{range}(f \\circ \\mathrm{Sum}.inr) $$$$

Lean4

theorem _root_.Sum.range_eq (f : α ⊕ β → γ) : range f = range (f ∘ Sum.inl) ∪ range (f ∘ Sum.inr) :=
  ext fun _ => Sum.exists

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