Monotone

📁 Source: Mathlib/Order/BoundedOrder/Monotone.lean

Statistics

Metric	Count
Definitions	0
Theorems ball, exists, forall, ball, exists, forall, apply_eq_bot_iff, apply_eq_top_iff, apply_eq_bot_iff, apply_eq_top_iff, maximal_preimage_top, minimal_preimage_bot, antitone_le, antitone_lt, forall_ge_iff, forall_le_iff, monotone_and, monotone_le, monotone_lt, monotone_or	20
Total	20

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ball 📖	—	Antitone PartialOrder.toPreorder Prop.partialOrder	—	—	—
exists 📖	—	Antitone PartialOrder.toPreorder Prop.partialOrder	—	—	—
forall 📖	—	Antitone PartialOrder.toPreorder Prop.partialOrder	—	—	—

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ball 📖	—	Monotone PartialOrder.toPreorder Prop.partialOrder	—	—	—
exists 📖	—	Monotone PartialOrder.toPreorder Prop.partialOrder	—	—	—
forall 📖	—	Monotone PartialOrder.toPreorder Prop.partialOrder	—	—	—

StrictAnti

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_bot_iff 📖	mathematical	StrictAnti PartialOrder.toPreorder	Bot.bot OrderBot.toBot Preorder.toLE	—	apply_eq_top_iff dual
apply_eq_top_iff 📖	mathematical	StrictAnti PartialOrder.toPreorder	Top.top OrderTop.toTop Preorder.toLE	—	not_lt_top_iff LT.lt.ne'

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_bot_iff 📖	mathematical	StrictMono PartialOrder.toPreorder	Bot.bot OrderBot.toBot Preorder.toLE	—	apply_eq_top_iff dual
apply_eq_top_iff 📖	mathematical	StrictMono PartialOrder.toPreorder	Top.top OrderTop.toTop Preorder.toLE	—	not_lt_top_iff LT.lt.ne
maximal_preimage_top 📖	—	StrictMono PartialOrder.toPreorder LinearOrder.toPartialOrder Top.top OrderTop.toTop Preorder.toLE	—	—	maximal_of_maximal_image le_top
minimal_preimage_bot 📖	—	StrictMono PartialOrder.toPreorder LinearOrder.toPartialOrder Bot.bot OrderBot.toBot Preorder.toLE	—	—	minimal_of_minimal_image bot_le

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitone_le 📖	mathematical	—	Antitone PartialOrder.toPreorder Prop.partialOrder Preorder.toLE	—	LE.le.trans
antitone_lt 📖	mathematical	—	Antitone PartialOrder.toPreorder Prop.partialOrder Preorder.toLT	—	LE.le.trans_lt
forall_ge_iff 📖	—	Monotone PartialOrder.toPreorder Prop.partialOrder	—	—	le_rfl
forall_le_iff 📖	—	Antitone PartialOrder.toPreorder Prop.partialOrder	—	—	le_rfl
monotone_and 📖	—	Monotone PartialOrder.toPreorder Prop.partialOrder	—	—	—
monotone_le 📖	mathematical	—	Monotone PartialOrder.toPreorder Prop.partialOrder Preorder.toLE	—	LE.le.trans
monotone_lt 📖	mathematical	—	Monotone PartialOrder.toPreorder Prop.partialOrder Preorder.toLT	—	LT.lt.trans_le
monotone_or 📖	—	Monotone PartialOrder.toPreorder Prop.partialOrder	—	—	—

---

← Back to Index