English
Let hc be IsRegular c and hι lift(#ι) < c. If hf ensures f i b < c.ord for all i and b < c.ord, then for all a < c.ord, derivFamily f a < c.ord.
Русский
Пусть hc: IsRegular c и hι: lift(#ι) < c. Тогда если hf обеспечивает f i b < c.ord для всех i и b < c.ord, то derivFamily f a < c.ord для каждого a < c.ord.
LaTeX
$$$IsRegular(c) \land \operatorname{lift}(\#ι) < c \Rightarrow ( \forall i, \forall b < \operatorname{ord}(c),\ f(i,b) < \operatorname{ord}(c) ) \Rightarrow \forall a < \operatorname{ord}(c),\operatorname{derivFamily}(f,a) < \operatorname{ord}(c)$$$
Lean4
/-- A cardinal is inaccessible if it is an uncountable regular strong limit cardinal. -/
def IsInaccessible (c : Cardinal) : Prop :=
ℵ₀ < c ∧ c ≤ c.ord.cof ∧ ∀ x < c, 2 ^ x < c
