principal_iff_of_monotone — Mathlib

English

If op is monotone in each argument, then Principal op o iff ∀ a < o, op(a,a) < o.

Русский

Если op монотонен по каждому аргументу, то Principal op o эквивалентно ∀ a < o, op(a,a) < o.

LaTeX

$$$$ \forall o, \forall op, \Big( \big( \forall a, \operatorname{Monotone}(op\,a) \big) \land \big( \forall a, \operatorname{Monotone}(\operatorname{Function.swap}(op)\ a) \big) \Rightarrow \operatorname{Principal}(op)\ o \iff \forall a

Lean4

theorem principal_iff_of_monotone (h₁ : ∀ a, Monotone (op a)) (h₂ : ∀ a, Monotone (Function.swap op a)) :
    Principal op o ↔ ∀ a < o, op a a < o := by
  use fun h a ha => h ha ha
  intro H a b ha hb
  obtain hab | hba := le_or_gt a b
  · exact (h₂ b hab).trans_lt <| H b hb
  · exact (h₁ a hba.le).trans_lt <| H a ha

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