comp — Mathlib

English

If g is an equidecomposition on B with T, f is an equidecomposition on A with S, and f maps A into B, then g ∘ f is an equidecomposition on A with T · S.

Русский

Если g — эквидекомпозиция на B с T, f — эквидекомпозиция на A с S и отображает A в B, то g ∘ f — эквидекомпозиция на A с индексами T · S.

LaTeX

$$$\\mathrm{IsDecompOn}(g,B,T) \\wedge \\mathrm{IsDecompOn}(f,A,S) \\wedge \\mathrm{MapsTo}(f,A,B) \\Rightarrow \\mathrm{IsDecompOn}(g\\circ f,\,A,\,T\\cdot S).$$$

Lean4

theorem comp {g f : X → X} {B A : Set X} {T S : Finset G} (hg : IsDecompOn g B T) (hf : IsDecompOn f A S)
    (h : MapsTo f A B) : IsDecompOn (g ∘ f) A (T * S) :=
  by
  rw [left_eq_inter.mpr h]
  exact hg.comp' hf

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