noMaxOrder_rank_toType — Mathlib

English

Under the assumed rank condition, there is no maximal order type for the ordinal corresponding to Module.rank F E.

Русский

При условии на ранги нет конечного максимального порядка для ординального типа Module.rank F E.

LaTeX

$$$$\\text{NoMaxOrder} \\big( (\\mathrm{Module.rank } F E).\\mathrm{ord.toType} \\big)$$$$

Lean4

theorem noMaxOrder_rank_toType : NoMaxOrder ι :=
  Cardinal.noMaxOrder Fact.out

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