Theorems · Theorem · order theory

WithBot.strictMono_iff

∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : WithBot α → β},
  StrictMono f ↔ (StrictMono fun a => f ↑a) ∧ ∀ (x : α), f ⊥ < f ↑x

Defined in

Mathlib.Order.WithBot

Cited by

2 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

PreorderPreorder