self

Mathlib.SetTheory.ZFC.Basic

URI: https://scilib.ai/kg/mathlib#ZFSet.Hereditarily.self

English

If x is hereditary with respect to p, then p holds for x.

Русский

Если x наследуется по p, то выполняется p(x).

LaTeX

$$$\\operatorname{Hereditarily}(p,x) \\Rightarrow p(x)$$$

Lean4

theorem self (h : x.Hereditarily p) : p x :=
  h.def.1

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

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

Разделы

Аффилиация

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