smash — Mathlib

English

If s1 ≃ t1 and s2 ≃ t2, with matching ends, then their Smashs are equivalent.

Русский

Если s1 эквивалентна t1 и s2 эквивалентна t2 и последние элементы совпадают, то их Smash эквивалентны.

LaTeX

$$$\\forall s_1\\ s_2\\ t_1\\ t_2,\\; hs : s_1.Equivalent t_1 \\land ht : s_2.Equivalent t_2 \\Rightarrow (smash s_1 s_2 hs) (smash t_1 t_2 ht).$$$

Lean4

protected theorem smash {s₁ s₂ t₁ t₂ : CompositionSeries X} (hs : s₁.last = s₂.head) (ht : t₁.last = t₂.head)
    (h₁ : Equivalent s₁ t₁) (h₂ : Equivalent s₂ t₂) : Equivalent (smash s₁ s₂ hs) (smash t₁ t₂ ht) :=
  let e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
    calc
      Fin (s₁.length + s₂.length) ≃ (Fin s₁.length) ⊕ (Fin s₂.length) := finSumFinEquiv.symm
      _ ≃ (Fin t₁.length) ⊕ (Fin t₂.length) := (Equiv.sumCongr h₁.choose h₂.choose)
      _ ≃ Fin (t₁.length + t₂.length) := finSumFinEquiv
  ⟨e, by
    intro i
    refine Fin.addCases ?_ ?_ i
    · intro i
      simpa [e, smash_castAdd, smash_succ_castAdd] using h₁.choose_spec i
    · intro i
      simpa [e, -Fin.castSucc_natAdd, smash_natAdd, smash_succ_natAdd] using h₂.choose_spec i⟩

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