Defs

📁 Source: Mathlib/Order/GaloisConnection/Defs.lean

Statistics

Metric	Count
Definitions `GaloisCoinsertion`, `choice`, `dual`, `monotoneIntro`, `ofDual`, `liftOrderBot`, `liftOrderTop`, `toGaloisCoinsertion`, `toGaloisInsertion`, `GaloisInsertion`, `choice`, `dual`, `monotoneIntro`, `ofDual`	14
Theorems `choice_eq`, `gc`, `l_injective`, `l_le_l_iff`, `strictMono_l`, `u_bot`, `u_l_eq`, `u_l_le`, `u_l_leftInverse`, `u_surjective`, `compose`, `dfun`, `dual`, `exists_eq_l`, `exists_eq_u`, `id`, `l_bot`, `l_comm_iff_u_comm`, `l_comm_of_u_comm`, `l_eq`, `l_eq_bot`, `l_le`, `l_u_bot`, `l_u_l_eq_l`, `l_u_l_eq_l'`, `l_u_le`, `l_u_le_trans`, `l_unique`, `le_iff_le`, `le_iff_le'`, `le_u`, `le_u_l`, `le_u_l_trans`, `lt_iff_lt`, `lt_iff_lt'`, `monotone_intro`, `monotone_l`, `monotone_u`, `u_comm_of_l_comm`, `u_eq`, `u_eq_top`, `u_l_top`, `u_l_u_eq_u`, `u_l_u_eq_u'`, `u_top`, `u_unique`, `choice_eq`, `gc`, `l_surjective`, `l_top`, `l_u_eq`, `le_l_u`, `leftInverse_l_u`, `strictMono_u`, `u_injective`, `u_le_u_iff`	56
Total	70

GaloisCoinsertion

Definitions

Name	Category	Theorems
`choice` 📖	CompOp	1 math math: `choice_eq`
`dual` 📖	CompOp	—
`monotoneIntro` 📖	CompOp	—
`ofDual` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`choice_eq` 📖	mathematical	`Preorder.toLE`	`choice`	—	—
`gc` 📖	mathematical	—	`GaloisConnection`	—	—
`l_injective` 📖	—	—	—	—	`GaloisInsertion.u_injective`
`l_le_l_iff` 📖	mathematical	—	`Preorder.toLE`	—	`GaloisInsertion.u_le_u_iff`
`strictMono_l` 📖	mathematical	—	`StrictMono`	—	`GaloisInsertion.strictMono_u`
`u_bot` 📖	mathematical	—	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder`	—	`GaloisInsertion.l_top`
`u_l_eq` 📖	—	—	—	—	`GaloisInsertion.l_u_eq`
`u_l_le` 📖	mathematical	—	`Preorder.toLE`	—	—
`u_l_leftInverse` 📖	—	—	—	—	`u_l_eq`
`u_surjective` 📖	—	—	—	—	`GaloisInsertion.l_surjective`

GaloisConnection

Definitions

Name	Category	Theorems
`liftOrderBot` 📖	CompOp	—
`liftOrderTop` 📖	CompOp	—
`toGaloisCoinsertion` 📖	CompOp	—
`toGaloisInsertion` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compose` 📖	—	`GaloisConnection`	—	—	—
`dfun` 📖	mathematical	`GaloisConnection`	`Pi.preorder`	—	—
`dual` 📖	mathematical	`GaloisConnection`	`OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `OrderDual.ofDual`	—	—
`exists_eq_l` 📖	—	`GaloisConnection` `PartialOrder.toPreorder`	—	—	`l_u_l_eq_l`
`exists_eq_u` 📖	—	`GaloisConnection` `PartialOrder.toPreorder`	—	—	`u_l_u_eq_u`
`id` 📖	mathematical	—	`GaloisConnection`	—	—
`l_bot` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder`	`Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	`l_eq_bot` `bot_le`
`l_comm_iff_u_comm` 📖	—	`GaloisConnection` `PartialOrder.toPreorder`	—	—	`l_comm_of_u_comm` `u_comm_of_l_comm`
`l_comm_of_u_comm` 📖	—	`GaloisConnection` `PartialOrder.toPreorder`	—	—	`l_unique` `compose`
`l_eq` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder`	`Preorder.toLE`	—	`LE.le.antisymm'` `le_u_l` `le_rfl`
`l_eq_bot` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder`	`Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	`le_bot_iff` `le_iff_le'`
`l_le` 📖	—	`GaloisConnection` `Preorder.toLE`	—	—	—
`l_u_bot` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder`	`Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	`l_eq_bot` `le_rfl`
`l_u_l_eq_l` 📖	—	`GaloisConnection` `PartialOrder.toPreorder`	—	—	`LE.le.antisymm'` `monotone_l` `le_u_l` `l_u_le`
`l_u_l_eq_l'` 📖	—	`GaloisConnection` `PartialOrder.toPreorder`	—	—	`l_u_l_eq_l`
`l_u_le` 📖	mathematical	`GaloisConnection`	`Preorder.toLE`	—	`l_le` `le_rfl`
`l_u_le_trans` 📖	—	`GaloisConnection` `Preorder.toLE`	—	—	`LE.le.trans'` `monotone_l` `le_u`
`l_unique` 📖	—	`GaloisConnection` `PartialOrder.toPreorder`	—	—	`ge_antisymm` `l_le` `le_u_l`
`le_iff_le` 📖	mathematical	`GaloisConnection`	`Preorder.toLE`	—	—
`le_iff_le'` 📖	mathematical	`GaloisConnection`	`Preorder.toLE`	—	—
`le_u` 📖	—	`GaloisConnection` `Preorder.toLE`	—	—	—
`le_u_l` 📖	mathematical	`GaloisConnection`	`Preorder.toLE`	—	`le_u` `le_rfl`
`le_u_l_trans` 📖	—	`GaloisConnection` `Preorder.toLE`	—	—	`LE.le.trans` `monotone_u` `l_le`
`lt_iff_lt` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	`Preorder.toLT`	—	`lt_iff_lt_of_le_iff_le`
`lt_iff_lt'` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	`Preorder.toLT`	—	`lt_iff_lt_of_le_iff_le`
`monotone_intro` 📖	mathematical	`Monotone` `Preorder.toLE`	`GaloisConnection`	—	`LE.le.trans`
`monotone_l` 📖	mathematical	`GaloisConnection`	`Monotone`	—	`l_le` `LE.le.trans'` `le_u_l`
`monotone_u` 📖	mathematical	`GaloisConnection`	`Monotone`	—	`le_u` `LE.le.trans` `l_u_le`
`u_comm_of_l_comm` 📖	—	`GaloisConnection` `PartialOrder.toPreorder`	—	—	`u_unique` `compose`
`u_eq` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder`	`Preorder.toLE`	—	`LE.le.antisymm` `l_u_le` `le_rfl`
`u_eq_top` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder`	`Top.top` `OrderTop.toTop` `Preorder.toLE`	—	`top_le_iff` `le_iff_le`
`u_l_top` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder`	`Top.top` `OrderTop.toTop` `Preorder.toLE`	—	`u_eq_top` `le_rfl`
`u_l_u_eq_u` 📖	—	`GaloisConnection` `PartialOrder.toPreorder`	—	—	`LE.le.antisymm` `monotone_u` `l_u_le` `le_u_l`
`u_l_u_eq_u'` 📖	—	`GaloisConnection` `PartialOrder.toPreorder`	—	—	`u_l_u_eq_u`
`u_top` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder`	`Top.top` `OrderTop.toTop` `Preorder.toLE`	—	`u_eq_top` `le_top`
`u_unique` 📖	—	`GaloisConnection` `PartialOrder.toPreorder`	—	—	`le_antisymm` `le_u` `l_u_le`

GaloisInsertion

Definitions

Name	Category	Theorems
`choice` 📖	CompOp	2 math math: `choice_eq`, `ContinuousMap.idealOpensGI_choice`
`dual` 📖	CompOp	—
`monotoneIntro` 📖	CompOp	—
`ofDual` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`choice_eq` 📖	mathematical	`Preorder.toLE`	`choice`	—	—
`gc` 📖	mathematical	—	`GaloisConnection`	—	—
`l_surjective` 📖	—	—	—	—	`Function.LeftInverse.surjective` `leftInverse_l_u`
`l_top` 📖	mathematical	—	`Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder`	—	`top_unique` `LE.le.trans` `le_l_u` `GaloisConnection.monotone_l` `gc` `le_top`
`l_u_eq` 📖	—	—	—	—	`LE.le.antisymm` `GaloisConnection.l_u_le` `gc` `le_l_u`
`le_l_u` 📖	mathematical	—	`Preorder.toLE`	—	—
`leftInverse_l_u` 📖	—	—	—	—	`l_u_eq`
`strictMono_u` 📖	mathematical	—	`StrictMono`	—	`strictMono_of_le_iff_le` `u_le_u_iff`
`u_injective` 📖	—	—	—	—	`leftInverse_l_u`
`u_le_u_iff` 📖	mathematical	—	`Preorder.toLE`	—	`LE.le.trans` `le_l_u` `GaloisConnection.l_le` `gc` `GaloisConnection.monotone_u`

(root)

Definitions

Name	Category	Theorems
`GaloisCoinsertion` 📖	CompData	—
`GaloisInsertion` 📖	CompData	—

---

← Back to Index