English
If g is an equidecomposition on B with T and f is an equidecomposition on A with S, then the composition g ∘ f is an equidecomposition on A ∩ f⁻¹(B) with the index set T · S.
Русский
Если g — эквидекомпозиция на B с множителями T, а f — эквидекомпозиция на A с множителями S, то композиция g ∘ f есть эквидекомпозиция на A ∩ f⁻¹(B) с индексами T · S.
LaTeX
$$$\\mathrm{IsDecompOn}(g,B,T) \\wedge \\mathrm{IsDecompOn}(f,A,S) \\Rightarrow \\mathrm{IsDecompOn}(g\\circ f,\,A\\cap f^{-1}(B),\,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) :
IsDecompOn (g ∘ f) (A ∩ f ⁻¹' B) (T * S) := by
intro _ ⟨aA, aB⟩
rcases hf _ aA with ⟨γ, γ_mem, hγ⟩
rcases hg _ aB with ⟨δ, δ_mem, hδ⟩
use δ * γ, Finset.mul_mem_mul δ_mem γ_mem
rwa [mul_smul, ← hγ]
