emultiplicity_lt_of_multiplicity_lt

English

If a and b satisfy FiniteMultiplicity and the multiplicity is less than n, then the emultiplicity is less than n.

Русский

Если a и b удовлетворяют FiniteMultiplicity и кратность меньше n, то эмплитичность меньше n.

LaTeX

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

Lean4

theorem emultiplicity_lt_of_multiplicity_lt (hfin : FiniteMultiplicity a b) {n : ℕ} (h : multiplicity a b < n) :
    emultiplicity a b < n := by
  rw [emultiplicity_eq_multiplicity hfin]
  assumption_mod_cast

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