funMap_equiv_unify — Mathlib

English

Equivalence in the DirectLimit setoid is independent of the representative choice.

Русский

Эквивалентность в множестве DirectLimit независима от выбранного представителя.

LaTeX

$$$\\text{Setoid }(\\Sigma^f)\\text{ is well-defined under the directed system}$$$

Lean4

theorem funMap_equiv_unify {n : ℕ} (F : L.Functions n) (x : Fin n → Σˣ f) (i : ι)
    (hi : i ∈ upperBounds (range (Sigma.fst ∘ x))) : funMap F x ≈ .mk f _ (funMap F (unify f x i hi)) :=
  funMap_unify_equiv G f F x (Classical.choose (Finite.bddAbove_range fun a => (x a).1)) i _ hi

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