SaddlePoint

📁 Source: Mathlib/Order/SaddlePoint.lean

Statistics

Metric	Count
Definitions IsSaddlePointOn	1
Theorems swap_left, swap_right, iSup₂_iInf₂_le_iInf₂_iSup₂, isSaddlePointOn_iff, isSaddlePointOn_iff', isSaddlePointOn_value	6
Total	7

IsSaddlePointOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
swap_left 📖	—	Set Set.instMembership IsSaddlePointOn	—	—	le_trans
swap_right 📖	—	Set Set.instMembership IsSaddlePointOn	—	—	swap_left

(root)

Definitions

Name	Category	Theorems
IsSaddlePointOn 📖	MathDef	2 math math: isSaddlePointOn_iff', isSaddlePointOn_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iSup₂_iInf₂_le_iInf₂_iSup₂ 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot Set Set.instMembership iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	iSup₂_le_iff le_iInf₂_iff iInf₂_le_of_le le_iSup₂_of_le le_refl
isSaddlePointOn_iff 📖	mathematical	Set Set.instMembership	IsSaddlePointOn PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	le_antisymm le_iSup₂ iInf₂_le
isSaddlePointOn_iff' 📖	mathematical	Set Set.instMembership	IsSaddlePointOn PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice Preorder.toLE iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	isSaddlePointOn_iff le_trans le_of_eq le_antisymm iInf₂_le le_iSup₂
isSaddlePointOn_value 📖	mathematical	Set Set.instMembership IsSaddlePointOn PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice	iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup	—	le_antisymm isSaddlePointOn_iff le_trans iInf₂_le le_rfl iInf₂_mono le_iSup₂ iSup₂_mono

---

← Back to Index