English
For f: WithBot α → β, StrictAnti f iff StrictAnti (λ a → f a) and ∀ x: α, f x < f ⊥.
Русский
Для f: WithBot α → β, StrictAnti f эквивалентно StrictAnti (λ a → f a) и ∀ x: α, f x < f ⊥.
LaTeX
$$$ \text{StrictAnti } f \iff \big( \text{StrictAnti } ( \lambda a: \alpha, f(a) ) \land \forall x: \alpha, f(x) < f(\bot) \big)$$$
Lean4
theorem strictAnti_iff {f : WithBot α → β} : StrictAnti f ↔ StrictAnti (fun a ↦ f a : α → β) ∧ ∀ x : α, f x < f ⊥ :=
strictMono_iff (β := βᵒᵈ)