initiallySmall_of_essentiallySmall

English

If J is EssentiallySmall, then InitiallySmall J, via an equivalence to a small model.

Русский

Если J является EssentiallySmall, то InitiallySmall J через эквивалентность малой модели.

LaTeX

$$$[\\text{EssentiallySmall } J] \\Rightarrow [\\text{InitiallySmall } J]$$$

Lean4

theorem initiallySmall_of_essentiallySmall [EssentiallySmall.{w} J] : InitiallySmall.{w} J :=
  InitiallySmall.mk' (equivSmallModel.{w} J).inverse

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