Monotone

📁 Source: Mathlib/Order/Interval/Set/Monotone.lean

Statistics

Metric	Count
Definitions	0
Theorems Ici, Ico, Iic, Iio, Ioc, Ioi, Ioo, Ici, Ico, Iic, Iio, Ioc, Ioi, Ioo, Ici, Ico, Iic, Iio, Ioc, Ioi, Ioo, Ici, Ico, Iic, Iio, Ioc, Ioi, Ioo, Ici_le_id, Iic_id_le, antitone_Ici, antitone_Ioi, iUnion_Ioo_of_mono_of_isGLB_of_isLUB, monotone_Iic, monotone_Iio, strictAntiOn_Ici_of_lt_pred, strictAntiOn_Iic_of_succ_lt, strictMonoOn_Ici_of_pred_lt, strictMonoOn_Iic_of_lt_succ	39
Total	39

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Ici 📖	mathematical	Antitone	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ici	—	comp antitone_Ici
Ico 📖	mathematical	Antitone Monotone	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ico	—	Monotone.inter Ici Monotone.Iio
Iic 📖	mathematical	Antitone	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Iic	—	Monotone.comp_antitone monotone_Iic
Iio 📖	mathematical	Antitone	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Iio	—	Monotone.comp_antitone monotone_Iio
Ioc 📖	mathematical	Antitone Monotone	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ioc	—	Monotone.inter Ioi Monotone.Iic
Ioi 📖	mathematical	Antitone	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ioi	—	comp antitone_Ioi
Ioo 📖	mathematical	Antitone Monotone	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ioo	—	Monotone.inter Ioi Monotone.Iio

AntitoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Ici 📖	mathematical	AntitoneOn	MonotoneOn Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ici	—	Antitone.comp_antitoneOn antitone_Ici
Ico 📖	mathematical	AntitoneOn MonotoneOn	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ico	—	MonotoneOn.inter Ici MonotoneOn.Iio
Iic 📖	mathematical	AntitoneOn	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Iic	—	Monotone.comp_antitoneOn monotone_Iic
Iio 📖	mathematical	AntitoneOn	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Iio	—	Monotone.comp_antitoneOn monotone_Iio
Ioc 📖	mathematical	AntitoneOn MonotoneOn	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ioc	—	MonotoneOn.inter Ioi MonotoneOn.Iic
Ioi 📖	mathematical	AntitoneOn	MonotoneOn Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ioi	—	Antitone.comp_antitoneOn antitone_Ioi
Ioo 📖	mathematical	AntitoneOn MonotoneOn	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ioo	—	MonotoneOn.inter Ioi MonotoneOn.Iio

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Ici 📖	mathematical	Monotone	Antitone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ici	—	Antitone.comp_monotone antitone_Ici
Ico 📖	mathematical	Monotone Antitone	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ico	—	Antitone.inter Ici Antitone.Iio
Iic 📖	mathematical	Monotone	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Iic	—	comp monotone_Iic
Iio 📖	mathematical	Monotone	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Iio	—	comp monotone_Iio
Ioc 📖	mathematical	Monotone Antitone	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ioc	—	Antitone.inter Ioi Antitone.Iic
Ioi 📖	mathematical	Monotone	Antitone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ioi	—	Antitone.comp_monotone antitone_Ioi
Ioo 📖	mathematical	Monotone Antitone	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ioo	—	Antitone.inter Ioi Antitone.Iio

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Ici 📖	mathematical	MonotoneOn	AntitoneOn Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ici	—	Antitone.comp_monotoneOn antitone_Ici
Ico 📖	mathematical	MonotoneOn AntitoneOn	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ico	—	AntitoneOn.inter Ici AntitoneOn.Iio
Iic 📖	mathematical	MonotoneOn	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Iic	—	Monotone.comp_monotoneOn monotone_Iic
Iio 📖	mathematical	MonotoneOn	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Iio	—	Monotone.comp_monotoneOn monotone_Iio
Ioc 📖	mathematical	MonotoneOn AntitoneOn	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ioc	—	AntitoneOn.inter Ioi AntitoneOn.Iic
Ioi 📖	mathematical	MonotoneOn	AntitoneOn Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ioi	—	Antitone.comp_monotoneOn antitone_Ioi
Ioo 📖	mathematical	MonotoneOn AntitoneOn	Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ioo	—	AntitoneOn.inter Ioi AntitoneOn.Iio

StrictMonoOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Ici_le_id 📖	—	StrictMonoOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ici Preorder.toLE	—	—	Iic_id_le instIsSuccArchimedeanOrderDual
Iic_id_le 📖	—	StrictMonoOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Iic Preorder.toLE	—	—	Succ.rec_bot LE.le.trans bot_le mono Set.Iic_subset_Iic Order.le_succ Order.succ_eq_iff_isMax Order.le_succ_iff_eq_or_le le_imp_le_of_le_of_le Order.succ_le_succ le_trans le_rfl le_refl Order.succ_le_of_lt Order.lt_succ_of_not_isMax

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitone_Ici 📖	mathematical	—	Antitone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ici	—	Set.Ici_subset_Ici
antitone_Ioi 📖	mathematical	—	Antitone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Ioi	—	Set.Ioi_subset_Ioi
iUnion_Ioo_of_mono_of_isGLB_of_isLUB 📖	mathematical	Antitone PartialOrder.toPreorder SemilatticeSup.toPartialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Monotone IsGLB Preorder.toLE Set.range IsLUB	Set.iUnion Set.Ioo	—	Set.iUnion_inter_of_monotone SemilatticeSup.instIsDirectedOrder Antitone.Ioi Monotone.Iio IsGLB.iUnion_Ioi_eq IsLUB.iUnion_Iio_eq
monotone_Iic 📖	mathematical	—	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Iic	—	Set.Iic_subset_Iic
monotone_Iio 📖	mathematical	—	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.Iio	—	Set.Iio_subset_Iio
strictAntiOn_Ici_of_lt_pred 📖	mathematical	Preorder.toLT Order.pred PartialOrder.toPreorder	StrictAntiOn Set.Ici	—	strictAntiOn_Iic_of_succ_lt instIsSuccArchimedeanOrderDual
strictAntiOn_Iic_of_succ_lt 📖	mathematical	Preorder.toLT Order.succ PartialOrder.toPreorder	StrictAntiOn Set.Iic	—	strictMonoOn_Iic_of_lt_succ
strictMonoOn_Ici_of_pred_lt 📖	mathematical	Preorder.toLT Order.pred PartialOrder.toPreorder	StrictMonoOn Set.Ici	—	strictMonoOn_Iic_of_lt_succ instIsSuccArchimedeanOrderDual
strictMonoOn_Iic_of_lt_succ 📖	mathematical	Preorder.toLT Order.succ PartialOrder.toPreorder	StrictMonoOn Set.Iic	—	strictMonoOn_of_lt_succ Set.ordConnected_Iic Order.succ_le_iff_of_not_isMax

---

← Back to Index