one_le_div_ae — Mathlib

English

@[to_additive] In additive setting, a.e. equality of f and g implies a.e. equality of f and g under division context.

Русский

В аддитивной записи, a.e. равенство функций при делении сохраняется.

LaTeX

$$$\text{(to_additive)}\; \text{div_ae_eq_one}.$$$

Lean4

@[to_additive sub_nonneg_ae]
theorem one_le_div_ae {β : Type*} [Group β] [LE β] [MulRightMono β] (f g : α → β) : 1 ≤ᵐ[μ] g / f ↔ f ≤ᵐ[μ] g :=
  by
  refine ⟨fun h ↦ h.mono fun a ha ↦ ?_, fun h ↦ h.mono fun a ha ↦ ?_⟩
  · rwa [Pi.one_apply, Pi.div_apply, one_le_div'] at ha
  · rwa [Pi.one_apply, Pi.div_apply, one_le_div']

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