emultiplicity_sub_of_gt — Mathlib

English

Assume emultiplicity p b < emultiplicity p a for p ∈ α. Then emultiplicity p (a − b) = emultiplicity p b.

Русский

Пусть для p ∈ α выполняется emultiplicity p b < emultiplicity p a. Тогда emultiplicity p (a − b) = emultiplicity p b.

LaTeX

$$$ \forall p,a,b \in \alpha, emultiplicity p b < emultiplicity p a \Rightarrow emultiplicity p (a-b) = emultiplicity p b $$$

Lean4

theorem emultiplicity_sub_of_gt {p a b : α} (h : emultiplicity p b < emultiplicity p a) :
    emultiplicity p (a - b) = emultiplicity p b := by
  rw [sub_eq_add_neg, emultiplicity_add_of_gt] <;> rw [emultiplicity_neg]; assumption

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