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_of_isDirected_le
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	Directed Preorder.toLE Function.extend Bot.bot Pi.instBotForall OrderBot.toBot	—	em Function.extend_apply' instReflLe Function.Injective.extend_apply
mono 📖	mathematical	Directed	Directed	—	—
mono_comp 📖	mathematical	Directed	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	DirectedOn Set.image	—	mono_comp mono
insert 📖	mathematical	Reflexive DirectedOn Set Set.instMembership	DirectedOn Set 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 📖	mathematical	DirectedOn Preorder.toLE Set Set.instMembership	Preorder.toLE	—	LE.le.trans'
is_top_of_is_max 📖	mathematical	DirectedOn Preorder.toLE Set Set.instMembership	Preorder.toLE	—	LE.le.trans
mono 📖	mathematical	DirectedOn	DirectedOn	—	mono'
mono' 📖	mathematical	DirectedOn	DirectedOn	—	—
mono_comp 📖	mathematical	DirectedOn	DirectedOn Set.image	—	directedOn_image mono
of_isCodirectedOrder 📖	mathematical	—	DirectedOn	—	directedOn_iff_isCodirectedOrder
of_isDirectedOrder 📖	mathematical	—	DirectedOn	—	directedOn_iff_isDirectedOrder
pi 📖	mathematical	DirectedOn	DirectedOn Set.pi Set.univ	—	—
prod 📖	mathematical	DirectedOn	DirectedOn SProd.sprod Set Set.instSProd	—	—
proj 📖	mathematical	DirectedOn	DirectedOn Set.image	—	mono_comp mono
snd 📖	mathematical	DirectedOn	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 Preorder.toLE	—	exists_ge_ge LE.le.trans
not_isMin 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder	IsMin Preorder.toLE PartialOrder.toPreorder	—	exists_lt_of_directed_le isTop IsMin.not_lt LE.le.antisymm
not_isMin' 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder	IsMin Preorder.toLE PartialOrder.toPreorder	—	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 Preorder.toLE	—	exists_le_le LE.le.trans'
not_isMax 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder	IsMax Preorder.toLE PartialOrder.toPreorder	—	exists_lt_of_directed_ge isBot IsMax.not_lt LE.le.antisymm'
not_isMax' 📖	mathematical	IsMin Preorder.toLE PartialOrder.toPreorder	IsMax Preorder.toLE PartialOrder.toPreorder	—	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_of_isDirected_ge
directed_le 📖	mathematical	Monotone	Directed Preorder.toLE	—	directed_of_isDirected_le
forall_le_of_antitone 📖	mathematical	Monotone Antitone Pi.hasLe Preorder.toLE	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	27 math math: RelHomClass.directed, FirstOrder.Language.directed_distinctConstantsTheory, Function.directed_ptsOfPeriod_pnat, Field.Emb.Cardinal.directed_filtration, Directed.mono, Module.End.genEigenspace_directed, IsChain.directed, Std.Total.directed, Directed.mono_comp, Directed.extend_bot, 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, Set.directed_dissipate, Antitone.directed_le, Set.directed_accumulate, directed_comp, Monotone.directed_le, TopCat.partialSections.directed, directed_id, directed_of_isDirected_ge
DirectedOn 📖	MathDef	47 math math: directedOn_ge_Ici, directedOn_le_Iic, DirectedOn.of_isDirectedOrder, directedOn_ge_Icc, directedOn_ge_Ico, DirectedOn.prod, Order.Ideal.directed', Std.Total.directedOn, IsGreatest.directedOn, directedOn_le_Ioc, Directed.directedOn_range, RelHomClass.directedOn, Order.IsIdeal.Directed, SupClosed.directedOn, Set.directedOn_sUnion, directedOn_image, Order.Ideal.directed, directedOn_iff_isCodirectedOrder, IsChain.directedOn, directedOn_le_Icc, directedOn_of_sup_mem, DirectedOn.mono', DirectedOn.mono_comp, directedOn_range, DirectedOn.fst, InfClosed.codirectedOn, directedOn_univ_iff, Order.PFilter.directed, directedOn_onFun_iff, DirectedOn.mono, directedOn_iff_isDirectedOrder, DirectedOn.pi, directedOn_iff_directed, DirectedOn.snd, directedOn_pair, Order.isIdeal_iff, IsLeast.directedOn, DirectedOn.of_isCodirectedOrder, DirectedOn.insert, CStarAlgebra.directedOn_nonneg_ball, directedOn_of_inf_mem, DirectedOn.proj, directedOn_singleton, directedOn_pair', Set.directedOn_iUnion, directedOn_univ, UniformOnFun.hasBasis_uniformity_of_basis_aux₂
IsCodirectedOrder 📖	MathDef	7 math math: Filter.atBot_neBot_iff, SemilatticeInf.instIsCodirectedOrder, directedOn_iff_isCodirectedOrder, instIsCodirectedOrder, DirectedOn.isCodirectedOrder, OrderDual.isDirected_ge, OrderBot.instIsCodirectedOrder
IsDirected 📖	CompData	6 math math: Std.Total.to_isDirected, CategoryTheory.IsFiltered.exists_directed, 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.mono_comp directed_id
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