strictAnti_iff — Mathlib

English

StrictAnti f iff StrictAnti on α and ∀ x, f ⊤ < f x.

Русский

StrictAnti f тогда и только тогда, когда StrictAnti на α и ∀ x, f ⊤ < f x.

LaTeX

$$$$ \\text{StrictAnti}(f) \\iff \\Big( \\text{StrictAnti}(\\lambda a: \\alpha, f a) \\land \\forall x: \\alpha, f \\top < f x \\Big). $$$$

Lean4

theorem strictAnti_iff {f : WithTop α → β} : StrictAnti f ↔ StrictAnti (fun a ↦ f a : α → β) ∧ ∀ x : α, f ⊤ < f x :=
  strictMono_iff (β := βᵒᵈ)

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