out_equiv — Mathlib

English

If F is definable and xs, ys are indexwise equivalent, then out F xs ≈ out F ys.

Русский

Если F определима, и xs, ys эквивалентны по каждому индексу, то out F xs эквивалентно out F ys.

LaTeX

$$$$ \forall n (f : (Fin n → ZFSet) → ZFSet) [Definable n f] {xs ys : Fin n → PSet} (h : \forall i, xs i ≈ ys i) : out f xs ≈ out f ys. $$$$

Lean4

theorem out_equiv {n} (f : (Fin n → ZFSet.{u}) → ZFSet.{u}) [Definable n f] {xs ys : Fin n → PSet}
    (h : ∀ i, xs i ≈ ys i) : out f xs ≈ out f ys :=
  by
  rw [← Quotient.eq_iff_equiv, mk_eq, mk_eq, mk_out, mk_out]
  exact congrArg _ (funext fun i ↦ Quotient.sound (h i))

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