Icc_eq — Mathlib

English

Icc f g equals the finsupp constructed from the per-coordinate intervals: Icc f g = (supp f ∪ supp g).finsupp (f.rangeIcc g).

Русский

Icc f g равен finsupp, строящейся из интервалов на каждой координате: Icc f g = (supp f ∪ supp g).finsupp (f.rangeIcc g).

LaTeX

$$$Icc\\;f\\;g = (\\operatorname{supp}(f) \\cup \\operatorname{supp}(g)).finsupp (f.rangeIcc g)$$$

Lean4

theorem Icc_eq : Icc f g = (f.support ∪ g.support).finsupp (f.rangeIcc g) :=
  rfl

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