English
If hAB = CovBySMul M K A B and hBC = CovBySMul N L B C, then CovBySMul N (K · L) A C holds under appropriate scalar action compatibility; i.e., composition of covering by cosets respects multiplication.
Русский
Если hAB = CovBySMul M K A B и hBC = CovBySMul N L B C, то CovBySMul N (K · L) A C выполняется, при условии совместимости скалярных действий; покрытие косетами сохраняется под умножением.
LaTeX
$$$$ \text{If } \mathrm{CovBySMul}(M,K,A,B) \text{ and } \mathrm{CovBySMul}(N,L,B,C), \ \mathrm{CovBySMul}(N,(K\cdot L),A,C). $$$$
Lean4
@[to_additive]
theorem trans [SMul M N] [IsScalarTower M N X] (hAB : CovBySMul M K A B) (hBC : CovBySMul N L B C) :
CovBySMul N (K * L) A C := by
classical
have := hAB.nonneg
obtain ⟨F₁, hF₁, hFAB⟩ := hAB
obtain ⟨F₂, hF₂, hFBC⟩ := hBC
refine ⟨F₁ • F₂, ?_, ?_⟩
·
calc
(#(F₁ • F₂) : ℝ) ≤ #F₁ * #F₂ := mod_cast Finset.card_smul_le
_ ≤ K * L := by gcongr
·
calc
A ⊆ (F₁ : Set M) • B := hFAB
_ ⊆ (F₁ : Set M) • (F₂ : Set N) • C := by gcongr
_ = (↑(F₁ • F₂) : Set N) • C := by simp
