lt_multiplicity_of_lt_emultiplicity

English

If FiniteMultiplicity a b and n < emultiplicity a b, then n < multiplicity a b.

Русский

Если FiniteMultiplicity a b и n < emultiplicity a b, то n < multiplicity a b.

LaTeX

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

Lean4

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

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