Embedding

📁 Source: Mathlib/Data/Fin/Tuple/Embedding.lean

Statistics

Metric	Count
Definitions append, cons, init, snoc, tail, embFinTwo, twoEmbeddingEquiv	7
Theorems coe_append, coe_cons, coe_snoc, coe_tail, init_snoc, snoc_castSucc, snoc_last, tail_cons, embFinTwo_apply_one, embFinTwo_apply_zero	10
Total	17

Fin.Embedding

Definitions

Name	Category	Theorems
append 📖	CompOp	1 math math: coe_append
cons 📖	CompOp	2 math math: coe_cons, tail_cons
init 📖	CompOp	1 math math: init_snoc
snoc 📖	CompOp	4 math math: init_snoc, coe_snoc, snoc_last, snoc_castSucc
tail 📖	CompOp	2 math math: tail_cons, coe_tail

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_append 📖	mathematical	Disjoint Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Set.instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	append Fin.append	—	—
coe_cons 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	cons Fin.cons	—	—
coe_snoc 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	snoc Fin.snoc	—	—
coe_tail 📖	mathematical	—	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding tail Fin.tail	—	—
init_snoc 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	init snoc	—	Fin.init_snoc
snoc_castSucc 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	snoc	—	coe_snoc Fin.snoc_castSucc
snoc_last 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	snoc	—	coe_snoc Fin.snoc_last
tail_cons 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	tail cons	—	—

Function.Embedding

Definitions

Name	Category	Theorems
embFinTwo 📖	CompOp	2 math math: embFinTwo_apply_zero, embFinTwo_apply_one
twoEmbeddingEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
embFinTwo_apply_one 📖	mathematical	—	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding embFinTwo	—	—
embFinTwo_apply_zero 📖	mathematical	—	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding embFinTwo	—	—

---

← Back to Index