strictAnti_iff — Mathlib

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 (β := βᵒᵈ)

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