instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition

English

If P.IsStableUnderComposition then precoverage respects composition of coverings, i.e., comp_mem_coverings holds.

Русский

Если P.IsStableUnderComposition, то precoverage сохраняет композицию покрытий.

LaTeX

$$instance : P.precoverage.IsStableUnderComposition where comp_mem_coverings {ι} S X f hf σ Y g hg Z p := by ...$$

Lean4

instance [P.IsStableUnderComposition] : P.precoverage.IsStableUnderComposition where
  comp_mem_coverings {ι} S X f hf σ Y g hg Z
    p := by
    intro ⟨i⟩
    exact P.comp_mem _ _ (hg _ ⟨i.2⟩) (hf ⟨i.1⟩)

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