out_equiv

Mathlib.SetTheory.ZFC.Basic

URI: https://scilib.ai/kg/mathlib#ZFSet.Definable₁.out_equiv

English

If x ≈ y and f is definable₁, then out f x ≈ out f y.

Русский

Если x ≈ y и f задаётся definable₁, то out f x ≈ out f y.

LaTeX

$$$$ (f) [Definable_1 f] {x y : PSet} (h : x \approx y) : out f x ≈ out f y. $$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru