OrdConnectedComponent

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

Statistics

Metric	Count
Definitions ordConnectedComponent, ordConnectedProj, ordConnectedSection, ordSeparatingSet, ordT5Nhd	5
Theorems disjoint_left_ordSeparatingSet, disjoint_ordT5Nhd, disjoint_right_ordSeparatingSet, dual_ordConnectedComponent, dual_ordConnectedSection, dual_ordSeparatingSet, eq_of_mem_ordConnectedSection_of_uIcc_subset, instOrdConnectedOrdConnectedComponent, mem_ordConnectedComponent, mem_ordConnectedComponent_comm, mem_ordConnectedComponent_ordConnectedProj, mem_ordConnectedComponent_trans, nonempty_ordConnectedComponent, ordConnectedComponent_empty, ordConnectedComponent_eq, ordConnectedComponent_eq_empty, ordConnectedComponent_inter, ordConnectedComponent_ordConnectedProj, ordConnectedComponent_subset, ordConnectedComponent_univ, ordConnectedProj_eq, ordConnectedProj_mem_ordConnectedComponent, ordConnectedSection_subset, ordSeparatingSet_comm, self_mem_ordConnectedComponent, subset_ordConnectedComponent	26
Total	31

Set

Definitions

Name	Category	Theorems
ordConnectedComponent 📖	CompOp	17 math math: self_mem_ordConnectedComponent, dual_ordConnectedComponent, mem_ordConnectedComponent_ordConnectedProj, subset_ordConnectedComponent, mem_ordConnectedComponent_comm, ordConnectedComponent_eq_empty, ordConnectedComponent_eq, ordConnectedComponent_empty, ordConnectedComponent_inter, ordConnectedComponent_subset, ordConnectedComponent_univ, ordConnectedComponent_ordConnectedProj, ordConnectedProj_mem_ordConnectedComponent, ordConnectedComponent_mem_nhds, instOrdConnectedOrdConnectedComponent, mem_ordConnectedComponent, nonempty_ordConnectedComponent
ordConnectedProj 📖	CompOp	4 math math: mem_ordConnectedComponent_ordConnectedProj, ordConnectedProj_eq, ordConnectedComponent_ordConnectedProj, ordConnectedProj_mem_ordConnectedComponent
ordConnectedSection 📖	CompOp	5 math math: compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE, dual_ordConnectedSection, compl_ordConnectedSection_ordSeparatingSet_mem_nhds, compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE, ordConnectedSection_subset
ordSeparatingSet 📖	CompOp	7 math math: compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE, disjoint_right_ordSeparatingSet, ordSeparatingSet_comm, compl_ordConnectedSection_ordSeparatingSet_mem_nhds, compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE, dual_ordSeparatingSet, disjoint_left_ordSeparatingSet
ordT5Nhd 📖	CompOp	2 math math: disjoint_ordT5Nhd, ordT5Nhd_mem_nhdsSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_left_ordSeparatingSet 📖	mathematical	—	Disjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice ordSeparatingSet	—	Disjoint.inter_right' disjoint_iUnion₂_right Disjoint.mono_right ordConnectedComponent_subset disjoint_compl_right
disjoint_ordT5Nhd 📖	mathematical	—	Disjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice ordT5Nhd	—	disjoint_iff_inf_le mem_iUnion₂ uIcc_subset_uIcc_union_uIcc union_subset uIcc_comm ordSeparatingSet_comm le_total Icc_subset_uIcc' Icc_subset_uIcc CanLift.prf Subtype.canLift uIcc_of_le mem_Icc not_lt disjoint_left disjoint_left_ordSeparatingSet LT.lt.le disjoint_right_ordSeparatingSet ordConnectedProj_mem_ordConnectedComponent mem_range_self subset_inter_iff mem_ordConnectedComponent le_of_not_ge
disjoint_right_ordSeparatingSet 📖	mathematical	—	Disjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice ordSeparatingSet	—	disjoint_left_ordSeparatingSet ordSeparatingSet_comm
dual_ordConnectedComponent 📖	mathematical	—	ordConnectedComponent OrderDual OrderDual.instLinearOrder preimage DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.toDual	—	ext Function.Surjective.forall Equiv.surjective uIcc_toDual EquivLike.range_eq_univ
dual_ordConnectedSection 📖	mathematical	—	ordConnectedSection OrderDual OrderDual.instLinearOrder preimage DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual	—	ext dual_ordConnectedComponent Nonempty.some.congr_simp
dual_ordSeparatingSet 📖	mathematical	—	ordSeparatingSet OrderDual OrderDual.instLinearOrder preimage DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual	—	iUnion_congr_Prop Function.Surjective.iUnion_comp Equiv.surjective dual_ordConnectedComponent preimage_iUnion
eq_of_mem_ordConnectedSection_of_uIcc_subset 📖	—	Set instMembership ordConnectedSection instHasSubset uIcc DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	ordConnectedProj_eq mem_ordConnectedComponent_trans ordConnectedProj_mem_ordConnectedComponent mem_ordConnectedComponent_ordConnectedProj
instOrdConnectedOrdConnectedComponent 📖	mathematical	—	OrdConnected PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ordConnectedComponent	—	ordConnected_of_uIcc_subset_left HasSubset.Subset.trans instIsTransSubset uIcc_subset_uIcc_left
mem_ordConnectedComponent 📖	mathematical	—	Set instMembership ordConnectedComponent instHasSubset uIcc DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—
mem_ordConnectedComponent_comm 📖	mathematical	—	Set instMembership ordConnectedComponent	—	mem_ordConnectedComponent uIcc_comm
mem_ordConnectedComponent_ordConnectedProj 📖	mathematical	—	Set instMembership ordConnectedComponent ordConnectedProj	—	mem_ordConnectedComponent_comm ordConnectedProj_mem_ordConnectedComponent
mem_ordConnectedComponent_trans 📖	—	Set instMembership ordConnectedComponent	—	—	uIcc_subset_uIcc_union_uIcc union_subset
nonempty_ordConnectedComponent 📖	mathematical	—	Nonempty ordConnectedComponent Set instMembership	—	left_mem_uIcc self_mem_ordConnectedComponent
ordConnectedComponent_empty 📖	mathematical	—	ordConnectedComponent Set instEmptyCollection	—	ordConnectedComponent_eq_empty notMem_empty
ordConnectedComponent_eq 📖	mathematical	Set instHasSubset uIcc DistribLattice.toLattice instDistribLatticeOfLinearOrder	ordConnectedComponent	—	ext mem_ordConnectedComponent_trans mem_ordConnectedComponent_comm
ordConnectedComponent_eq_empty 📖	mathematical	—	ordConnectedComponent Set instEmptyCollection instMembership	—	not_nonempty_iff_eq_empty nonempty_ordConnectedComponent
ordConnectedComponent_inter 📖	mathematical	—	ordConnectedComponent Set instInter	—	—
ordConnectedComponent_ordConnectedProj 📖	mathematical	—	ordConnectedComponent ordConnectedProj Set instMembership	—	ordConnectedComponent_eq mem_ordConnectedComponent_ordConnectedProj
ordConnectedComponent_subset 📖	mathematical	—	Set instHasSubset ordConnectedComponent	—	right_mem_uIcc
ordConnectedComponent_univ 📖	mathematical	—	ordConnectedComponent univ	—	—
ordConnectedProj_eq 📖	mathematical	—	ordConnectedProj Set instHasSubset uIcc DistribLattice.toLattice instDistribLatticeOfLinearOrder instMembership	—	mem_ordConnectedComponent ordConnectedComponent_ordConnectedProj self_mem_ordConnectedComponent ordConnectedComponent_eq Nonempty.some.congr_simp
ordConnectedProj_mem_ordConnectedComponent 📖	mathematical	—	Set instMembership ordConnectedComponent ordConnectedProj	—	Nonempty.some_mem
ordConnectedSection_subset 📖	mathematical	—	Set instHasSubset ordConnectedSection	—	range_subset_iff ordConnectedComponent_subset Nonempty.some_mem
ordSeparatingSet_comm 📖	mathematical	—	ordSeparatingSet	—	inter_comm
self_mem_ordConnectedComponent 📖	mathematical	—	Set instMembership ordConnectedComponent	—	mem_ordConnectedComponent uIcc_self singleton_subset_iff
subset_ordConnectedComponent 📖	mathematical	Set instMembership instHasSubset	ordConnectedComponent	—	HasSubset.Subset.trans instIsTransSubset OrdConnected.uIcc_subset

---

← Back to Index