Interval

📁 Source: Mathlib/Data/Sum/Interval.lean

Statistics

Metric	Count
Definitions `sumLexLift`, `sumLift₂`, `instLocallyFiniteOrderBot`, `instLocallyFiniteOrderTop`, `locallyFiniteOrder`, `instLocallyFiniteOrder`, `instLocallyFiniteOrderBot`, `instLocallyFiniteOrderTop`	8
Theorems `inl_mem_sumLexLift`, `inl_mem_sumLift₂`, `inr_mem_sumLexLift`, `inr_mem_sumLift₂`, `mem_sumLexLift`, `mem_sumLift₂`, `sumLexLift_eq_empty`, `sumLexLift_inl_inl`, `sumLexLift_inl_inr`, `sumLexLift_inr_inl`, `sumLexLift_inr_inr`, `sumLexLift_mono`, `sumLexLift_nonempty`, `sumLift₂_eq_empty`, `sumLift₂_mono`, `sumLift₂_nonempty`, `Icc_inl_inl`, `Icc_inl_inr`, `Icc_inr_inl`, `Icc_inr_inr`, `Ici_inl`, `Ici_inr`, `Ico_inl_inl`, `Ico_inl_inr`, `Ico_inr_inl`, `Ico_inr_inr`, `Iic_inl`, `Iic_inr`, `Iio_inl`, `Iio_inr`, `Ioc_inl_inl`, `Ioc_inl_inr`, `Ioc_inr_inl`, `Ioc_inr_inr`, `Ioi_inl`, `Ioi_inr`, `Ioo_inl_inl`, `Ioo_inl_inr`, `Ioo_inr_inl`, `Ioo_inr_inr`, `Icc_inl_inl`, `Icc_inl_inr`, `Icc_inr_inl`, `Icc_inr_inr`, `Ici_inl`, `Ici_inr`, `Ico_inl_inl`, `Ico_inl_inr`, `Ico_inr_inl`, `Ico_inr_inr`, `Iic_inl`, `Iic_inr`, `Iio_inl`, `Iio_inr`, `Ioc_inl_inl`, `Ioc_inl_inr`, `Ioc_inr_inl`, `Ioc_inr_inr`, `Ioi_inl`, `Ioi_inr`, `Ioo_inl_inl`, `Ioo_inl_inr`, `Ioo_inr_inl`, `Ioo_inr_inr`	64
Total	72

Finset

Definitions

Name	Category	Theorems
`sumLexLift` 📖	CompOp	10 math math: `sumLexLift_inr_inl`, `inr_mem_sumLexLift`, `sumLexLift_nonempty`, `sumLexLift_eq_empty`, `sumLexLift_inl_inl`, `inl_mem_sumLexLift`, `mem_sumLexLift`, `sumLexLift_mono`, `sumLexLift_inr_inr`, `sumLexLift_inl_inr`
`sumLift₂` 📖	CompOp	6 math math: `mem_sumLift₂`, `sumLift₂_eq_empty`, `inl_mem_sumLift₂`, `inr_mem_sumLift₂`, `sumLift₂_mono`, `sumLift₂_nonempty`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inl_mem_sumLexLift` 📖	mathematical	—	`Finset` `instMembership` `sumLexLift`	—	—
`inl_mem_sumLift₂` 📖	mathematical	—	`Finset` `instMembership` `sumLift₂`	—	`mem_sumLift₂`
`inr_mem_sumLexLift` 📖	mathematical	—	`Finset` `instMembership` `sumLexLift`	—	—
`inr_mem_sumLift₂` 📖	mathematical	—	`Finset` `instMembership` `sumLift₂`	—	`mem_sumLift₂`
`mem_sumLexLift` 📖	mathematical	—	`Finset` `instMembership` `sumLexLift`	—	`sumLexLift.eq_1` `mem_map` `mem_disjSum` `notMem_empty` `Sum.inr_injective` `sumLexLift.eq_4` `mem_map_of_mem` `inl_mem_disjSum` `inr_mem_disjSum`
`mem_sumLift₂` 📖	mathematical	—	`Finset` `instMembership` `sumLift₂`	—	`sumLift₂.eq_1` `mem_map` `notMem_empty` `sumLift₂.eq_4` `mem_map_of_mem`
`sumLexLift_eq_empty` 📖	mathematical	—	`sumLexLift` `Finset` `instEmptyCollection`	—	`map_eq_empty` `disjSum_eq_empty` `Sum.inr_injective` `disjSum_empty`
`sumLexLift_inl_inl` 📖	mathematical	—	`sumLexLift` `map` `Function.Embedding.inl`	—	—
`sumLexLift_inl_inr` 📖	mathematical	—	`sumLexLift` `disjSum`	—	—
`sumLexLift_inr_inl` 📖	mathematical	—	`sumLexLift` `Finset` `instEmptyCollection`	—	—
`sumLexLift_inr_inr` 📖	mathematical	—	`sumLexLift` `map` `Sum.inr_injective`	—	—
`sumLexLift_mono` 📖	mathematical	`Finset` `instHasSubset`	`sumLexLift`	—	`map_subset_map` `disjSum_mono` `Subset.rfl` `Sum.inr_injective`
`sumLexLift_nonempty` 📖	mathematical	—	`Nonempty` `sumLexLift`	—	—
`sumLift₂_eq_empty` 📖	mathematical	—	`sumLift₂` `Finset` `instEmptyCollection`	—	`map_eq_empty`
`sumLift₂_mono` 📖	mathematical	`Finset` `instHasSubset`	`sumLift₂`	—	`map_subset_map` `Subset.rfl`
`sumLift₂_nonempty` 📖	mathematical	—	`Nonempty` `sumLift₂`	—	—

Sum

Definitions

Name	Category	Theorems
`instLocallyFiniteOrder` 📖	CompOp	16 math math: `Ico_inl_inl`, `Ioc_inl_inr`, `Ioo_inl_inr`, `Icc_inr_inr`, `Ioc_inr_inr`, `Ioo_inr_inr`, `Ioo_inr_inl`, `Icc_inl_inr`, `Ioo_inl_inl`, `Ico_inr_inr`, `Icc_inr_inl`, `Ico_inl_inr`, `Ioc_inr_inl`, `Ioc_inl_inl`, `Ico_inr_inl`, `Icc_inl_inl`
`instLocallyFiniteOrderBot` 📖	CompOp	4 math math: `Iio_inr`, `Iio_inl`, `Iic_inl`, `Iic_inr`
`instLocallyFiniteOrderTop` 📖	CompOp	4 math math: `Ici_inr`, `Ioi_inr`, `Ici_inl`, `Ioi_inl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_inl_inl` 📖	mathematical	—	`Finset.Icc` `instPreorderSum` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.inl`	—	—
`Icc_inl_inr` 📖	mathematical	—	`Finset.Icc` `instPreorderSum` `instLocallyFiniteOrder` `Finset` `Finset.instEmptyCollection`	—	—
`Icc_inr_inl` 📖	mathematical	—	`Finset.Icc` `instPreorderSum` `instLocallyFiniteOrder` `Finset` `Finset.instEmptyCollection`	—	—
`Icc_inr_inr` 📖	mathematical	—	`Finset.Icc` `instPreorderSum` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.inr`	—	—
`Ici_inl` 📖	mathematical	—	`Finset.Ici` `instPreorderSum` `instLocallyFiniteOrderTop` `Finset.map` `Function.Embedding.inl`	—	—
`Ici_inr` 📖	mathematical	—	`Finset.Ici` `instPreorderSum` `instLocallyFiniteOrderTop` `Finset.map` `Function.Embedding.inr`	—	—
`Ico_inl_inl` 📖	mathematical	—	`Finset.Ico` `instPreorderSum` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.inl`	—	—
`Ico_inl_inr` 📖	mathematical	—	`Finset.Ico` `instPreorderSum` `instLocallyFiniteOrder` `Finset` `Finset.instEmptyCollection`	—	—
`Ico_inr_inl` 📖	mathematical	—	`Finset.Ico` `instPreorderSum` `instLocallyFiniteOrder` `Finset` `Finset.instEmptyCollection`	—	—
`Ico_inr_inr` 📖	mathematical	—	`Finset.Ico` `instPreorderSum` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.inr`	—	—
`Iic_inl` 📖	mathematical	—	`Finset.Iic` `instPreorderSum` `instLocallyFiniteOrderBot` `Finset.map` `Function.Embedding.inl`	—	—
`Iic_inr` 📖	mathematical	—	`Finset.Iic` `instPreorderSum` `instLocallyFiniteOrderBot` `Finset.map` `Function.Embedding.inr`	—	—
`Iio_inl` 📖	mathematical	—	`Finset.Iio` `instPreorderSum` `instLocallyFiniteOrderBot` `Finset.map` `Function.Embedding.inl`	—	—
`Iio_inr` 📖	mathematical	—	`Finset.Iio` `instPreorderSum` `instLocallyFiniteOrderBot` `Finset.map` `Function.Embedding.inr`	—	—
`Ioc_inl_inl` 📖	mathematical	—	`Finset.Ioc` `instPreorderSum` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.inl`	—	—
`Ioc_inl_inr` 📖	mathematical	—	`Finset.Ioc` `instPreorderSum` `instLocallyFiniteOrder` `Finset` `Finset.instEmptyCollection`	—	—
`Ioc_inr_inl` 📖	mathematical	—	`Finset.Ioc` `instPreorderSum` `instLocallyFiniteOrder` `Finset` `Finset.instEmptyCollection`	—	—
`Ioc_inr_inr` 📖	mathematical	—	`Finset.Ioc` `instPreorderSum` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.inr`	—	—
`Ioi_inl` 📖	mathematical	—	`Finset.Ioi` `instPreorderSum` `instLocallyFiniteOrderTop` `Finset.map` `Function.Embedding.inl`	—	—
`Ioi_inr` 📖	mathematical	—	`Finset.Ioi` `instPreorderSum` `instLocallyFiniteOrderTop` `Finset.map` `Function.Embedding.inr`	—	—
`Ioo_inl_inl` 📖	mathematical	—	`Finset.Ioo` `instPreorderSum` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.inl`	—	—
`Ioo_inl_inr` 📖	mathematical	—	`Finset.Ioo` `instPreorderSum` `instLocallyFiniteOrder` `Finset` `Finset.instEmptyCollection`	—	—
`Ioo_inr_inl` 📖	mathematical	—	`Finset.Ioo` `instPreorderSum` `instLocallyFiniteOrder` `Finset` `Finset.instEmptyCollection`	—	—
`Ioo_inr_inr` 📖	mathematical	—	`Finset.Ioo` `instPreorderSum` `instLocallyFiniteOrder` `Finset.map` `Function.Embedding.inr`	—	—

Sum.Lex

Definitions

Name	Category	Theorems
`instLocallyFiniteOrderBot` 📖	CompOp	4 math math: `Iic_inr`, `Iio_inl`, `Iic_inl`, `Iio_inr`
`instLocallyFiniteOrderTop` 📖	CompOp	4 math math: `Ioi_inr`, `Ici_inl`, `Ioi_inl`, `Ici_inr`
`locallyFiniteOrder` 📖	CompOp	16 math math: `Icc_inr_inr`, `Ico_inl_inl`, `Ico_inr_inr`, `Ioo_inl_inr`, `Ioo_inr_inl`, `Ioo_inr_inr`, `Icc_inl_inl`, `Ioc_inl_inl`, `Icc_inr_inl`, `Ioc_inl_inr`, `Ioc_inr_inl`, `Ioc_inr_inr`, `Ioo_inl_inl`, `Ico_inr_inl`, `Ico_inl_inr`, `Icc_inl_inr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_inl_inl` 📖	mathematical	—	`Finset.Icc` `Lex` `preorder` `locallyFiniteOrder` `Sum.inlₗ` `Finset.map` `Function.Embedding.trans` `Function.Embedding.inl` `Equiv.toEmbedding` `toLex`	—	`Finset.map_map`
`Icc_inl_inr` 📖	mathematical	—	`Finset.Icc` `Lex` `preorder` `locallyFiniteOrder` `Sum.inlₗ` `Sum.inrₗ` `Finset.map` `Equiv.toEmbedding` `toLex` `Finset.disjSum` `Finset.Ici` `Finset.Iic`	—	—
`Icc_inr_inl` 📖	mathematical	—	`Finset.Icc` `Lex` `preorder` `locallyFiniteOrder` `Sum.inrₗ` `Sum.inlₗ` `Finset` `Finset.instEmptyCollection`	—	—
`Icc_inr_inr` 📖	mathematical	—	`Finset.Icc` `Lex` `preorder` `locallyFiniteOrder` `Sum.inrₗ` `Finset.map` `Function.Embedding.trans` `Function.Embedding.inr` `Equiv.toEmbedding` `toLex`	—	`Finset.map_map`
`Ici_inl` 📖	mathematical	—	`Finset.Ici` `Lex` `preorder` `instLocallyFiniteOrderTop` `Sum.inlₗ` `Finset.map` `Equiv.toEmbedding` `toLex` `Finset.disjSum` `Finset.univ`	—	—
`Ici_inr` 📖	mathematical	—	`Finset.Ici` `Lex` `preorder` `instLocallyFiniteOrderTop` `Sum.inrₗ` `Finset.map` `Function.Embedding.trans` `Function.Embedding.inr` `Equiv.toEmbedding` `toLex`	—	—
`Ico_inl_inl` 📖	mathematical	—	`Finset.Ico` `Lex` `preorder` `locallyFiniteOrder` `Sum.inlₗ` `Finset.map` `Function.Embedding.trans` `Function.Embedding.inl` `Equiv.toEmbedding` `toLex`	—	`Finset.map_map`
`Ico_inl_inr` 📖	mathematical	—	`Finset.Ico` `Lex` `preorder` `locallyFiniteOrder` `Sum.inlₗ` `Sum.inrₗ` `Finset.map` `Equiv.toEmbedding` `toLex` `Finset.disjSum` `Finset.Ici` `Finset.Iio`	—	—
`Ico_inr_inl` 📖	mathematical	—	`Finset.Ico` `Lex` `preorder` `locallyFiniteOrder` `Sum.inrₗ` `Sum.inlₗ` `Finset` `Finset.instEmptyCollection`	—	—
`Ico_inr_inr` 📖	mathematical	—	`Finset.Ico` `Lex` `preorder` `locallyFiniteOrder` `Sum.inrₗ` `Finset.map` `Function.Embedding.trans` `Function.Embedding.inr` `Equiv.toEmbedding` `toLex`	—	`Finset.map_map`
`Iic_inl` 📖	mathematical	—	`Finset.Iic` `Lex` `preorder` `instLocallyFiniteOrderBot` `Sum.inlₗ` `Finset.map` `Function.Embedding.trans` `Function.Embedding.inl` `Equiv.toEmbedding` `toLex`	—	—
`Iic_inr` 📖	mathematical	—	`Finset.Iic` `Lex` `preorder` `instLocallyFiniteOrderBot` `Sum.inrₗ` `Finset.map` `Equiv.toEmbedding` `toLex` `Finset.disjSum` `Finset.univ`	—	—
`Iio_inl` 📖	mathematical	—	`Finset.Iio` `Lex` `preorder` `instLocallyFiniteOrderBot` `Sum.inlₗ` `Finset.map` `Function.Embedding.trans` `Function.Embedding.inl` `Equiv.toEmbedding` `toLex`	—	—
`Iio_inr` 📖	mathematical	—	`Finset.Iio` `Lex` `preorder` `instLocallyFiniteOrderBot` `Sum.inrₗ` `Finset.map` `Equiv.toEmbedding` `toLex` `Finset.disjSum` `Finset.univ`	—	—
`Ioc_inl_inl` 📖	mathematical	—	`Finset.Ioc` `Lex` `preorder` `locallyFiniteOrder` `Sum.inlₗ` `Finset.map` `Function.Embedding.trans` `Function.Embedding.inl` `Equiv.toEmbedding` `toLex`	—	`Finset.map_map`
`Ioc_inl_inr` 📖	mathematical	—	`Finset.Ioc` `Lex` `preorder` `locallyFiniteOrder` `Sum.inlₗ` `Sum.inrₗ` `Finset.map` `Equiv.toEmbedding` `toLex` `Finset.disjSum` `Finset.Ioi` `Finset.Iic`	—	—
`Ioc_inr_inl` 📖	mathematical	—	`Finset.Ioc` `Lex` `preorder` `locallyFiniteOrder` `Sum.inrₗ` `Sum.inlₗ` `Finset` `Finset.instEmptyCollection`	—	—
`Ioc_inr_inr` 📖	mathematical	—	`Finset.Ioc` `Lex` `preorder` `locallyFiniteOrder` `Sum.inrₗ` `Finset.map` `Function.Embedding.trans` `Function.Embedding.inr` `Equiv.toEmbedding` `toLex`	—	`Finset.map_map`
`Ioi_inl` 📖	mathematical	—	`Finset.Ioi` `Lex` `preorder` `instLocallyFiniteOrderTop` `Sum.inlₗ` `Finset.map` `Equiv.toEmbedding` `toLex` `Finset.disjSum` `Finset.univ`	—	—
`Ioi_inr` 📖	mathematical	—	`Finset.Ioi` `Lex` `preorder` `instLocallyFiniteOrderTop` `Sum.inrₗ` `Finset.map` `Function.Embedding.trans` `Function.Embedding.inr` `Equiv.toEmbedding` `toLex`	—	—
`Ioo_inl_inl` 📖	mathematical	—	`Finset.Ioo` `Lex` `preorder` `locallyFiniteOrder` `Sum.inlₗ` `Finset.map` `Function.Embedding.trans` `Function.Embedding.inl` `Equiv.toEmbedding` `toLex`	—	`Finset.map_map`
`Ioo_inl_inr` 📖	mathematical	—	`Finset.Ioo` `Lex` `preorder` `locallyFiniteOrder` `Sum.inlₗ` `Sum.inrₗ` `Finset.map` `Equiv.toEmbedding` `toLex` `Finset.disjSum` `Finset.Ioi` `Finset.Iio`	—	—
`Ioo_inr_inl` 📖	mathematical	—	`Finset.Ioo` `Lex` `preorder` `locallyFiniteOrder` `Sum.inrₗ` `Sum.inlₗ` `Finset` `Finset.instEmptyCollection`	—	—
`Ioo_inr_inr` 📖	mathematical	—	`Finset.Ioo` `Lex` `preorder` `locallyFiniteOrder` `Sum.inrₗ` `Finset.map` `Function.Embedding.trans` `Function.Embedding.inr` `Equiv.toEmbedding` `toLex`	—	`Finset.map_map`

---

← Back to Index