piCongrLeft — Mathlib

English

Moving a dependent type along an equivalence of coordinates yields a measurable equivalence: piCongrLeft (f : δ ≃ δ') gives (∀ b, π (f b)) ≃ᵐ ∀ a, π a.

Русский

Перемещение зависимого типа вдоль эквивалентности координат даёт измеримое эквивалентность пространств функций: piCongrLeft (f) : (∀ b, π (f b)) ≃ᵐ (∀ a, π a).

LaTeX

$$$ \text{piCongrLeft } f : (\forall b, \pi (f b)) \simeq^ᵐ (\forall a, \pi a) $$$

Lean4

/-- Moving a dependent type along an equivalence of coordinates, as a measurable equivalence. -/
def piCongrLeft (f : δ ≃ δ') : (∀ b, π (f b)) ≃ᵐ ∀ a, π a
    where
  __ := Equiv.piCongrLeft π f
  measurable_toFun := measurable_piCongrLeft f
  measurable_invFun := by
    rw [measurable_pi_iff]
    exact fun i => measurable_pi_apply (f i)

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