Interval

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

Statistics

Metric	Count
Definitions instLocallyFiniteOrder	1
Theorems Icc_eq_finset_subtype, Ico_eq_finset_subtype, Ioc_eq_finset_subtype, Ioo_eq_finset_subtype, card_Icc, card_Ico, card_Ioc, card_Ioo, card_fintype_Icc, card_fintype_Ico, card_fintype_Ioc, card_fintype_Ioo, card_fintype_uIcc, card_uIcc, map_subtype_embedding_Icc, map_subtype_embedding_Ico, map_subtype_embedding_Ioc, map_subtype_embedding_Ioo, map_subtype_embedding_uIcc, uIcc_eq_finset_subtype	20
Total	21

PNat

Definitions

Name	Category	Theorems
instLocallyFiniteOrder 📖	CompOp	20 math math: map_subtype_embedding_Ico, Icc_eq_finset_subtype, Ioo_eq_finset_subtype, card_Icc, Ico_eq_finset_subtype, card_fintype_uIcc, map_subtype_embedding_Icc, uIcc_eq_finset_subtype, card_Ico, map_subtype_embedding_Ioo, Ioc_eq_finset_subtype, map_subtype_embedding_uIcc, card_fintype_Ioo, card_uIcc, card_Ioo, card_fintype_Ioc, card_fintype_Ico, card_Ioc, map_subtype_embedding_Ioc, card_fintype_Icc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_eq_finset_subtype 📖	mathematical	—	Finset.Icc PNat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder Finset.subtype Nat.instPreorder Nat.instLocallyFiniteOrder val	—	—
Ico_eq_finset_subtype 📖	mathematical	—	Finset.Ico PNat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder Finset.subtype Nat.instPreorder Nat.instLocallyFiniteOrder val	—	—
Ioc_eq_finset_subtype 📖	mathematical	—	Finset.Ioc PNat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder Finset.subtype Nat.instPreorder Nat.instLocallyFiniteOrder val	—	—
Ioo_eq_finset_subtype 📖	mathematical	—	Finset.Ioo PNat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder Finset.subtype Nat.instPreorder Nat.instLocallyFiniteOrder val	—	—
card_Icc 📖	mathematical	—	Finset.card PNat Finset.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder val	—	Nat.card_Icc map_subtype_embedding_Icc Finset.card_map
card_Ico 📖	mathematical	—	Finset.card PNat Finset.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder val	—	Nat.card_Ico map_subtype_embedding_Ico Finset.card_map
card_Ioc 📖	mathematical	—	Finset.card PNat Finset.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder val	—	Nat.card_Ioc map_subtype_embedding_Ioc Finset.card_map
card_Ioo 📖	mathematical	—	Finset.card PNat Finset.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder val	—	Nat.card_Ioo map_subtype_embedding_Ioo Finset.card_map
card_fintype_Icc 📖	mathematical	—	Fintype.card Set.Elem PNat Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat Set.instFintypeIcc instLocallyFiniteOrder val	—	card_Icc Finset.mem_Icc Fintype.card_ofFinset
card_fintype_Ico 📖	mathematical	—	Fintype.card Set.Elem PNat Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat Set.instFintypeIco instLocallyFiniteOrder val	—	card_Ico Finset.mem_Ico Fintype.card_ofFinset
card_fintype_Ioc 📖	mathematical	—	Fintype.card Set.Elem PNat Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat Set.instFintypeIoc instLocallyFiniteOrder val	—	card_Ioc Finset.mem_Ioc Fintype.card_ofFinset
card_fintype_Ioo 📖	mathematical	—	Fintype.card Set.Elem PNat Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat Set.instFintypeIoo instLocallyFiniteOrder val	—	card_Ioo Finset.mem_Ioo Fintype.card_ofFinset
card_fintype_uIcc 📖	mathematical	—	Fintype.card Set.Elem PNat Set.uIcc DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat Set.fintypeUIcc instLocallyFiniteOrder val	—	card_uIcc Finset.mem_uIcc Fintype.card_ofFinset
card_uIcc 📖	mathematical	—	Finset.card PNat Finset.uIcc DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder val	—	Nat.card_uIcc map_subtype_embedding_uIcc Finset.card_map
map_subtype_embedding_Icc 📖	mathematical	—	Finset.map Function.Embedding.subtype Finset.Icc PNat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder Nat.instPreorder Nat.instLocallyFiniteOrder val	—	Finset.map_subtype_embedding_Icc LT.lt.trans_le
map_subtype_embedding_Ico 📖	mathematical	—	Finset.map Function.Embedding.subtype Finset.Ico PNat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder Nat.instPreorder Nat.instLocallyFiniteOrder val	—	Finset.map_subtype_embedding_Ico LT.lt.trans_le
map_subtype_embedding_Ioc 📖	mathematical	—	Finset.map Function.Embedding.subtype Finset.Ioc PNat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder Nat.instPreorder Nat.instLocallyFiniteOrder val	—	Finset.map_subtype_embedding_Ioc LT.lt.trans_le
map_subtype_embedding_Ioo 📖	mathematical	—	Finset.map Function.Embedding.subtype Finset.Ioo PNat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder Nat.instPreorder Nat.instLocallyFiniteOrder val	—	Finset.map_subtype_embedding_Ioo LT.lt.trans_le
map_subtype_embedding_uIcc 📖	mathematical	—	Finset.map Function.Embedding.subtype Finset.uIcc PNat DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder instDistribLatticeNat Nat.instLocallyFiniteOrder val	—	map_subtype_embedding_Icc
uIcc_eq_finset_subtype 📖	mathematical	—	Finset.uIcc PNat DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat instLocallyFiniteOrder Finset.subtype instDistribLatticeNat Nat.instLocallyFiniteOrder val	—	—

---

← Back to Index