sigmaComparison_comp_sigmaIso — Mathlib

English

A symmetric version of the previous induction principle that assumes symmetry of P and that P(x,y) implies P(-x,y); it yields a full induction on Ereals with symmetry negation.

Русский

Симметрическая версия предыдущего принципа индукции, предполагающая симметрию P и что P(x,y) ⇒ P(-x,y); обеспечивает полную индукцию по Ereals с учетом отрицания.

LaTeX

$$$\text{Induction₂_symm_neg} := \forall P\, (P\text{ симметрично})\,.\,.$$

Lean4

theorem sigmaComparison_comp_sigmaIso [HasExplicitFiniteCoproducts.{u} P] (X : (CompHausLike.{u} P)ᵒᵖ ⥤ Type max u w) :
    (X.mapIso (sigmaIso r).op).hom ≫ sigmaComparison X (fun a ↦ (fiber r a).1) ≫ (fun g ↦ g a) =
      X.map (sigmaIncl r a).op :=
  by
  ext
  simp only [Functor.mapIso_hom, Iso.op_hom, types_comp_apply, sigmaComparison, ← FunctorToTypes.map_comp_apply]
  rfl

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