relMap_equiv_unify — Mathlib

English

There is an induction principle for the DirectLimit: to prove a property for all elements, it suffices to verify it on each component using the embedding to the limit.

Русский

Существующий принцип индукции для прямого предела: чтобы доказать свойство для любого элемента, достаточно проверить его на каждом компоненте через вложение к пределу.

LaTeX

$$$\\forall z:\\mathrm{DirectLimit}\;G f,\\; (\\forall i,x,\\; C(\\mathrm{of}(i,x)) ) \\Rightarrow C(z)$$$

Lean4

theorem relMap_equiv_unify {n : ℕ} (R : L.Relations n) (x : Fin n → Σˣ f) (i : ι)
    (hi : i ∈ upperBounds (range (Sigma.fst ∘ x))) : RelMap R x = RelMap R (unify f x i hi) :=
  relMap_unify_equiv G f R x (Classical.choose (Finite.bddAbove_range fun a => (x a).1)) i _ hi

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