Directed

📁 Source: Mathlib/Order/Directed.lean

Statistics

Metric	Count
Definitions `Directed`, `DirectedOn`, `IsCodirectedOrder`, `IsDirected`, `IsDirectedOrder`	5
Theorems `directed_ge`, `directed_le`, `directedOn_range`, `extend_bot`, `mono`, `mono_comp`, `directed_val`, `fst`, `insert`, `isCodirectedOrder`, `isDirectedOrder`, `is_bot_of_is_min`, `is_top_of_is_max`, `mono`, `mono'`, `mono_comp`, `of_isCodirectedOrder`, `of_isDirectedOrder`, `pi`, `prod`, `proj`, `snd`, `directed`, `isTop`, `not_isMin`, `not_isMin'`, `isBot`, `not_isMax`, `not_isMax'`, `directed_ge`, `directed_le`, `forall_le_of_antitone`, `Directed`, `instIsCodirectedOrder`, `isDirected_ge`, `isDirected_le`, `instIsDirectedOrder`, `instIsCodirectedOrder`, `instIsDirectedOrder`, `directed`, `directedOn`, `to_isDirected`, `constant_of_monotoneOn_antitoneOn`, `constant_of_monotone_antitone`, `directedOn_iff_directed`, `directedOn_iff_isCodirectedOrder`, `directedOn_iff_isDirectedOrder`, `directedOn_image`, `directedOn_of_inf_mem`, `directedOn_of_sup_mem`, `directedOn_onFun_iff`, `directedOn_pair`, `directedOn_pair'`, `directedOn_range`, `directedOn_singleton`, `directedOn_univ`, `directedOn_univ_iff`, `directed_comp`, `directed_id`, `directed_id_iff`, `directed_of`, `directed_of_isDirected_ge`, `directed_of_isDirected_le`, `directed_of₃`, `exists_ge_ge`, `exists_le_le`, `exists_lt_of_directed_ge`, `exists_lt_of_directed_le`, `isBot_iff_isMin`, `isBot_or_exists_lt`, `isDirected_mono`, `isTop_iff_isMax`, `isTop_or_exists_gt`	73
Total	78

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directed_ge` 📖	mathematical	`Antitone`	`Directed` `Preorder.toLE`	—	—
`directed_le` 📖	mathematical	`Antitone`	`Directed` `Preorder.toLE`	—	`directed_of_isDirected_ge`

Directed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directedOn_range` 📖	mathematical	`Directed`	`DirectedOn` `Set.range`	—	`directedOn_range`
`extend_bot` 📖	mathematical	`Directed` `Preorder.toLE`	`Function.extend` `Bot.bot` `Pi.instBotForall` `OrderBot.toBot`	—	`em` `Function.extend_apply'` `Function.Injective.extend_apply`
`mono` 📖	—	`Directed`	—	—	—
`mono_comp` 📖	—	`Directed`	—	—	`directed_comp` `mono`

DirectedOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directed_val` 📖	mathematical	`DirectedOn`	`Directed` `Set` `Set.instMembership`	—	`directedOn_iff_directed`
`fst` 📖	mathematical	`DirectedOn`	`Set.image`	—	`mono_comp` `mono`
`insert` 📖	mathematical	`Reflexive` `DirectedOn` `Set` `Set.instMembership`	`Set.instInsert`	—	`Set.mem_insert` `Set.mem_insert_of_mem`
`isCodirectedOrder` 📖	mathematical	`DirectedOn`	`IsCodirectedOrder` `Set.Elem` `Set` `Set.instMembership`	—	`directedOn_iff_isCodirectedOrder`
`isDirectedOrder` 📖	mathematical	`DirectedOn`	`IsDirectedOrder` `Set.Elem` `Set` `Set.instMembership`	—	`directedOn_iff_isDirectedOrder`
`is_bot_of_is_min` 📖	—	`DirectedOn` `Preorder.toLE` `Set` `Set.instMembership`	—	—	`LE.le.trans'`
`is_top_of_is_max` 📖	—	`DirectedOn` `Preorder.toLE` `Set` `Set.instMembership`	—	—	`LE.le.trans`
`mono` 📖	—	`DirectedOn`	—	—	`mono'`
`mono'` 📖	—	`DirectedOn`	—	—	—
`mono_comp` 📖	mathematical	`DirectedOn`	`Set.image`	—	`directedOn_image` `mono`
`of_isCodirectedOrder` 📖	mathematical	—	`DirectedOn`	—	`directedOn_iff_isCodirectedOrder`
`of_isDirectedOrder` 📖	mathematical	—	`DirectedOn`	—	`directedOn_iff_isDirectedOrder`
`pi` 📖	mathematical	`DirectedOn`	`Set.pi` `Set.univ`	—	—
`prod` 📖	mathematical	`DirectedOn`	`SProd.sprod` `Set` `Set.instSProd`	—	—
`proj` 📖	mathematical	`DirectedOn`	`Set.image`	—	`mono_comp` `mono`
`snd` 📖	mathematical	`DirectedOn`	`Set.image`	—	`mono_comp` `mono`

IsDirected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directed` 📖	—	—	—	—	—

IsMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTop` 📖	mathematical	`IsMax` `Preorder.toLE`	`IsTop`	—	`exists_ge_ge` `LE.le.trans`
`not_isMin` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder`	`IsMin`	—	`exists_lt_of_directed_le` `isTop` `IsMin.not_lt` `LE.le.antisymm`
`not_isMin'` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder`	`IsMin`	—	`not_isMin` `OrderDual.instNontrivial` `OrderDual.isDirected_le` `IsMin.toDual` `toDual`

IsMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBot` 📖	mathematical	`IsMin` `Preorder.toLE`	`IsBot`	—	`exists_le_le` `LE.le.trans'`
`not_isMax` 📖	mathematical	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder`	`IsMax`	—	`exists_lt_of_directed_ge` `isBot` `IsMax.not_lt` `LE.le.antisymm'`
`not_isMax'` 📖	mathematical	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder`	`IsMax`	—	`not_isMax` `OrderDual.instNontrivial` `OrderDual.isDirected_ge` `IsMax.toDual` `toDual`

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directed_ge` 📖	mathematical	`Monotone`	`Directed` `Preorder.toLE`	—	—
`directed_le` 📖	mathematical	`Monotone`	`Directed` `Preorder.toLE`	—	`directed_of_isDirected_le`
`forall_le_of_antitone` 📖	—	`Monotone` `Antitone` `Pi.hasLe` `Preorder.toLE`	—	—	`exists_ge_ge`

Order.IsIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Directed` 📖	mathematical	`Order.IsIdeal`	`DirectedOn`	—	—

OrderBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCodirectedOrder` 📖	mathematical	—	`IsCodirectedOrder`	—	`bot_le`

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isDirected_ge` 📖	mathematical	—	`IsCodirectedOrder` `OrderDual` `instLE`	—	—
`isDirected_le` 📖	mathematical	—	`IsDirectedOrder` `OrderDual` `instLE`	—	—

OrderTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsDirectedOrder` 📖	mathematical	—	`IsDirectedOrder`	—	`le_top`

SemilatticeInf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCodirectedOrder` 📖	mathematical	—	`IsCodirectedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `toPartialOrder`	—	`inf_le_left` `inf_le_right`

SemilatticeSup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsDirectedOrder` 📖	mathematical	—	`IsDirectedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `toPartialOrder`	—	`le_sup_left` `le_sup_right`

Std.Total

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directed` 📖	mathematical	—	`Directed`	—	`total_of` `refl`
`directedOn` 📖	mathematical	—	`DirectedOn`	—	`total_of` `refl`
`to_isDirected` 📖	mathematical	—	`IsDirected`	—	`directed_id_iff` `directed`

(root)

Definitions

Name	Category	Theorems
`Directed` 📖	MathDef	21 math math: `FirstOrder.Language.directed_distinctConstantsTheory`, `Function.directed_ptsOfPeriod_pnat`, `Field.Emb.Cardinal.directed_filtration`, `Module.End.genEigenspace_directed`, `IsChain.directed`, `Std.Total.directed`, `Antitone.directed_ge`, `directed_of_isDirected_le`, `directedOn_range`, `OmegaCompletePartialOrder.Chain.directed`, `DirectedOn.directed_val`, `CategoryTheory.Functor.ranges_directed`, `directed_id_iff`, `Monotone.directed_ge`, `directedOn_iff_directed`, `Antitone.directed_le`, `directed_comp`, `Monotone.directed_le`, `TopCat.partialSections.directed`, `directed_id`, `directed_of_isDirected_ge`
`DirectedOn` 📖	MathDef	34 math math: `directedOn_ge_Ici`, `directedOn_le_Iic`, `DirectedOn.of_isDirectedOrder`, `directedOn_ge_Icc`, `directedOn_ge_Ico`, `Order.Ideal.directed'`, `Std.Total.directedOn`, `IsGreatest.directedOn`, `directedOn_le_Ioc`, `Directed.directedOn_range`, `Order.IsIdeal.Directed`, `SupClosed.directedOn`, `directedOn_image`, `Order.Ideal.directed`, `directedOn_iff_isCodirectedOrder`, `IsChain.directedOn`, `directedOn_le_Icc`, `directedOn_of_sup_mem`, `directedOn_range`, `InfClosed.codirectedOn`, `directedOn_univ_iff`, `Order.PFilter.directed`, `directedOn_onFun_iff`, `directedOn_iff_isDirectedOrder`, `directedOn_iff_directed`, `directedOn_pair`, `Order.isIdeal_iff`, `IsLeast.directedOn`, `DirectedOn.of_isCodirectedOrder`, `CStarAlgebra.directedOn_nonneg_ball`, `directedOn_of_inf_mem`, `directedOn_singleton`, `directedOn_pair'`, `directedOn_univ`
`IsCodirectedOrder` 📖	MathDef	7 math math: `Filter.atBot_neBot_iff`, `SemilatticeInf.instIsCodirectedOrder`, `directedOn_iff_isCodirectedOrder`, `instIsCodirectedOrder`, `DirectedOn.isCodirectedOrder`, `OrderDual.isDirected_ge`, `OrderBot.instIsCodirectedOrder`
`IsDirected` 📖	CompData	5 math math: `Std.Total.to_isDirected`, `directedOn_univ_iff`, `directed_id_iff`, `isDirected_mono`, `Finset.isDirected_subset`
`IsDirectedOrder` 📖	MathDef	10 math math: `CategoryTheory.IsFiltered.isDirectedOrder`, `OrderDual.isDirected_le`, `directedOn_iff_isDirectedOrder`, `OrderTop.instIsDirectedOrder`, `Finset.isDirected_le`, `SemilatticeSup.instIsDirectedOrder`, `Module.fgSystem.instIsDirectedOrderSubtypeSubmoduleFG`, `Filter.atTop_neBot_iff`, `DirectedOn.isDirectedOrder`, `instIsDirectedOrder`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`constant_of_monotoneOn_antitoneOn` 📖	—	`MonotoneOn` `PartialOrder.toPreorder` `AntitoneOn` `DirectedOn` `Preorder.toLE` `Set` `Set.instMembership`	—	—	`le_antisymm` `LE.le.trans`
`constant_of_monotone_antitone` 📖	—	`Monotone` `PartialOrder.toPreorder` `Antitone`	—	—	`Monotone.forall_le_of_antitone` `le_rfl` `le_antisymm`
`directedOn_iff_directed` 📖	mathematical	—	`DirectedOn` `Directed` `Set` `Set.instMembership`	—	—
`directedOn_iff_isCodirectedOrder` 📖	mathematical	—	`DirectedOn` `IsCodirectedOrder` `Set.Elem` `Set` `Set.instMembership`	—	`directedOn_iff_directed` `IsCodirectedOrder.eq_1`
`directedOn_iff_isDirectedOrder` 📖	mathematical	—	`DirectedOn` `IsDirectedOrder` `Set.Elem` `Set` `Set.instMembership`	—	`directedOn_iff_directed` `IsDirectedOrder.eq_1`
`directedOn_image` 📖	mathematical	—	`DirectedOn` `Set.image` `Order.Preimage`	—	—
`directedOn_of_inf_mem` 📖	mathematical	`Set` `Set.instMembership` `SemilatticeInf.toMin`	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	`directedOn_of_sup_mem`
`directedOn_of_sup_mem` 📖	mathematical	`Set` `Set.instMembership` `SemilatticeSup.toMax`	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`le_sup_left` `le_sup_right`
`directedOn_onFun_iff` 📖	mathematical	—	`DirectedOn` `Function.onFun` `Set.image`	—	`DirectedOn.mono_comp` `Set.mem_image_of_mem`
`directedOn_pair` 📖	mathematical	`Reflexive`	`DirectedOn` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`DirectedOn.insert` `directedOn_singleton`
`directedOn_pair'` 📖	mathematical	`Reflexive`	`DirectedOn` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`Set.pair_comm` `directedOn_pair`
`directedOn_range` 📖	mathematical	—	`Directed` `DirectedOn` `Set.range`	—	—
`directedOn_singleton` 📖	mathematical	`Reflexive`	`DirectedOn` `Set` `Set.instSingletonSet`	—	—
`directedOn_univ` 📖	mathematical	—	`DirectedOn` `Set.univ`	—	`directed_of`
`directedOn_univ_iff` 📖	mathematical	—	`DirectedOn` `Set.univ` `IsDirected`	—	`directedOn_univ`
`directed_comp` 📖	mathematical	—	`Directed` `Order.Preimage`	—	—
`directed_id` 📖	mathematical	—	`Directed`	—	`directed_of`
`directed_id_iff` 📖	mathematical	—	`Directed` `IsDirected`	—	`directed_id`
`directed_of` 📖	—	—	—	—	`IsDirected.directed`
`directed_of_isDirected_ge` 📖	mathematical	—	`Directed`	—	`directed_of_isDirected_le` `OrderDual.isDirected_le`
`directed_of_isDirected_le` 📖	mathematical	—	`Directed`	—	`Directed.mono_comp` `directed_id`
`directed_of₃` 📖	—	—	—	—	`directed_of`
`exists_ge_ge` 📖	—	—	—	—	`directed_of`
`exists_le_le` 📖	—	—	—	—	`directed_of`
`exists_lt_of_directed_ge` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder`	—	`exists_pair_ne` `isBot_or_exists_lt` `LE.le.lt_of_ne`
`exists_lt_of_directed_le` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder`	—	`exists_pair_ne` `isTop_or_exists_gt` `LE.le.lt_of_ne'`
`isBot_iff_isMin` 📖	mathematical	—	`IsBot` `Preorder.toLE` `IsMin`	—	`IsBot.isMin` `IsMin.isBot`
`isBot_or_exists_lt` 📖	mathematical	—	`IsBot` `Preorder.toLE` `Preorder.toLT`	—	`IsMin.isBot` `not_isMin_iff` `em`
`isDirected_mono` 📖	mathematical	—	`IsDirected`	—	`IsDirected.directed`
`isTop_iff_isMax` 📖	mathematical	—	`IsTop` `Preorder.toLE` `IsMax`	—	`IsTop.isMax` `IsMax.isTop`
`isTop_or_exists_gt` 📖	mathematical	—	`IsTop` `Preorder.toLE` `Preorder.toLT`	—	`IsMax.isTop` `not_isMax_iff` `em`

---

← Back to Index