H0_induction_on — Mathlib

English

There is an elimination/induction principle for H0: to prove a property for any element of H0(A) it suffices to prove it on representatives coming from invariants via the H0Iso A inverse.

Русский

Для H0(A) существует принцип устранения/индукции: чтобы доказать свойство для любого элемента H0(A) достаточно доказать его для представителей, получаемых через обратное отображение H0Iso A.

LaTeX

$$H0_induction_on(A) : ∀{C:H0 A → Prop}(x:H0 A), (∀x'∈A.ρ.invariants, C((H0Iso A)^{-1} x')) → C x$$

Lean4

@[elab_as_elim]
theorem H0_induction_on {C : H0 A → Prop} (x : H0 A) (h : ∀ x : A.ρ.invariants, C ((H0Iso A).inv x)) : C x := by
  simpa using h ((H0Iso A).hom x)

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