English
Let hc be IsRegular c and hι < 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ι < c. Тогда hf обеспечивает f i b < c.ord для всех i и b < c.ord, значит for all a< c.ord, derivFamily f a < c.ord.
LaTeX
$$$IsRegular(c) \land hι < 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
@[deprecated "use the default constructor for `IsInaccessible`" (since := "2025-07-01")]
theorem mk {c} (h₁ : ℵ₀ < c) (h₂ : c ≤ c.ord.cof) (h₃ : ∀ x < c, (2 ^ x) < c) : IsInaccessible c :=
⟨h₁, h₂, h₃⟩
