reindex — Mathlib

English

If an equivalence e: α' ≃ α and P: EffectiveEpiFamily (λa', X (e a')) (λa', π (e a')) then EffectiveEpiFamily X π.

Русский

Если имеется эквивалентность e: α' ≃ α и P: EffectiveEpiFamily (X (e a')) (π (e a')), то существует EffectiveEpiFamily X π.

LaTeX

$$$\big(\text{EffectiveEpiFamily}(\lambda a' : α'.\, X( e a'))(\lambda a' : α'.\, π(e a'))\big) \Rightarrow \operatorname{EffectiveEpiFamily} X π$$$

Lean4

/-- Reindex the indexing type of an effective epi family.
-/
theorem reindex {B : C} {α α' : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) (e : α' ≃ α)
    (h : EffectiveEpiFamily (fun a => X (e a)) (fun a => π (e a))) : EffectiveEpiFamily X π :=
  .mk <| .intro <| @EffectiveEpiFamily.getStruct _ _ _ _ _ _ h |>.reindex _ _ e

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