out_equiv — Mathlib

English

If x1 ≈ y1 and x2 ≈ y2, then out f x1 x2 ≈ out f y1 y2 for definable₂ f.

Русский

Если x1 ≈ y1 и x2 ≈ y2, то out f x1 x2 ≈ out f y1 y2 для definable₂ f.

LaTeX

$$$$ (f) [Definable_2 f] {x1 y1 x2 y2 : PSet} (h1 : x1 ≈ y1) (h2 : x2 ≈ y2) : out f x1 x2 ≈ out f y1 y2. $$$$

Lean4

theorem out_equiv (f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) [Definable₂ f] {x₁ y₁ x₂ y₂ : PSet} (h₁ : x₁ ≈ y₁)
    (h₂ : x₂ ≈ y₂) : out f x₁ x₂ ≈ out f y₁ y₂ :=
  Definable.out_equiv _ (by simp [Fin.forall_fin_succ, h₁, h₂])

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