div_left — Mathlib

English

If f1 antivaries with g and f2 monovaries with g on s, then f1 / f2 antivaries with g on s.

Русский

Если f1 антивариантно варьируется с g, а f2 монообразно варьируется с g на s, то f1 / f2 антивариантно варьируется с g на s.

LaTeX

$$$$\\operatorname{AntivaryOn}(f_1, g, s) \\land \\operatorname{MonovaryOn}(f_2, g, s) \\Rightarrow \\operatorname{AntivaryOn}\\left(\\frac{f_1}{f_2}, g, s\\right).$$$$

Lean4

@[to_additive]
theorem div_left (h₁ : Antivary f₁ g) (h₂ : Monovary f₂ g) : Antivary (f₁ / f₂) g := fun _i _j hij ↦
  div_le_div'' (h₁ hij) (h₂ hij)

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