English
Let p be a property of ZF sets and x a ZF set. A set x is hereditary with respect to p if p holds for x and for every element y of x, y is hereditary with respect to p. Then x is hereditary with respect to p if and only if p(x) holds and every member of x is hereditary with respect to p.
Русский
Пусть p — свойство ZF-множества, и x — ZF-множество. Множество x называется наследуемым по p, если выполняются p(x) и для каждого элемента y ∈ x верно, что y наследуется по p. Тогда x наследуется по p тогда, когда p(x) и все элементы x наследуются по p.
LaTeX
$$$\\operatorname{Hereditarily}(p,x) \\leftrightarrow p(x) \\land \\forall y \\in x\\, \\operatorname{Hereditarily}(p,y)$$$
Lean4
theorem hereditarily_iff : Hereditarily p x ↔ p x ∧ ∀ y ∈ x, Hereditarily p y := by rw [← Hereditarily]
