embeddingCongr_apply_trans — Mathlib

English

For equivalences ea, eb, ec and embeddings f, g, the action of embeddingCongr distributes over trans.

Русский

Для эквивалентностей ea, eb, ec и вложений f, g согласование вложений распределяется через трансформацию.

LaTeX

$$$\\text{embeddingCongr }e_a e_c (f \\!\\mathrm{.trans}\\! g) = (\\text{embeddingCongr }e_a e_b f) \\!\\mathrm{trans}\\! (\\text{embeddingCongr }e_b e_c g)$$$

Lean4

theorem embeddingCongr_apply_trans {α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂)
    (f : α₁ ↪ β₁) (g : β₁ ↪ γ₁) :
    Equiv.embeddingCongr ea ec (f.trans g) = (Equiv.embeddingCongr ea eb f).trans (Equiv.embeddingCongr eb ec g) :=
  by
  ext
  simp

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