congr_apply_of — Mathlib

English

The ring-direct limit enjoys an induction principle: a property holds on the whole limit if it holds on the images of all components.

Русский

Предел по кольцам имеет индукционный принцип: свойство верно на всем пределе, если оно верно на образах всех компонент.

LaTeX

$$$\forall z:\; \text{Ring.DirectLimit}(G,f),\; C(z) \iff \forall i\; x\; C(\text{of}(G,f,i,x))$$$

Lean4

theorem congr_apply_of (e : (i : ι) → G i ≃+ G' i)
    (he : ∀ i j h, (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp (e i)) {i : ι} (g : G i) :
    congr e he (of G f i g) = of G' f' i (e i g) :=
  map_apply_of _ he _

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