inducedMap_inducedMap — Mathlib

English

The induced maps compose: for any a ∈ α, inducedMap β γ ( inducedMap α β a ) = inducedMap α γ a.

Русский

Индуцированные отображения композиционно: для любого a ∈ α, indMap_{β,γ}( indMap_{α,β}(a) ) = indMap_{α,γ}(a).

LaTeX

$$$\\operatorname{inducedMap}_{\\beta,\\gamma}(\\operatorname{inducedMap}_{\\alpha,\\beta}(a)) = \\operatorname{inducedMap}_{\\alpha,\\gamma}(a)$$$

Lean4

@[simp]
theorem inducedMap_inducedMap (a : α) : inducedMap β γ (inducedMap α β a) = inducedMap α γ a :=
  eq_of_forall_rat_lt_iff_lt fun q => by
    rw [coe_lt_inducedMap_iff, coe_lt_inducedMap_iff, Iff.comm, coe_lt_inducedMap_iff]

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