lt_emultiplicity_of_lt_multiplicity

English

For any natural number n, if n is less than the multiplicity of a and b, then n is less than the emultiplicity of a and b.

Русский

Для любого натурального n, если n меньше кратности a и b, то n меньше эмплитичности a и b.

LaTeX

$$$$\forall {\alpha} [Monoid \alpha] \; {a,b: \alpha} ,\; \forall {n: \mathbb{N}},\; n < multiplicity\ a\ b \rightarrow n < emultiplicity\ a\ b.$$$$

Lean4

theorem lt_emultiplicity_of_lt_multiplicity {n : ℕ} (h : n < multiplicity a b) : n < emultiplicity a b := by
  exact_mod_cast (WithTop.coe_strictMono h).trans_le multiplicity_le_emultiplicity

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