Tree

📁 Source: Mathlib/SetTheory/Descriptive/Tree.lean

Statistics

Metric	Count
Definitions drop, instTransListSubtypeSetMemCompleteSublatticeTreeIsPrefix, pullSub, subAt, take, instPartialOrderSubtypeSetListMemCompleteSublatticeTree, instSetLikeSubtypeSetListMemCompleteSublatticeTree, tree, Tree	9
Theorems drop_coe, mem_of_append, mem_of_prefix, mem_pullSub_append, mem_pullSub_long, mem_pullSub_self, mem_pullSub_short, mem_subAt, pullSub_adjunction, pullSub_append, pullSub_mono, pullSub_nil, pullSub_subAt, singleton_mem, subAt_append, subAt_mono, subAt_nil, subAt_pullSub, take_coe, take_eq_take, take_mem, take_take, tree_eq_bot, coe_def	24
Total	33

Descriptive

Definitions

Name	Category	Theorems
instPartialOrderSubtypeSetListMemCompleteSublatticeTree 📖	CompOp	—
instSetLikeSubtypeSetListMemCompleteSublatticeTree 📖	CompOp	11 math math: Tree.take_mem, Tree.mem_pullSub_long, Tree.take_coe, coe_def, Tree.take_eq_take, Tree.tree_eq_bot, Tree.mem_subAt, Tree.mem_pullSub_self, Tree.mem_pullSub_short, Tree.drop_coe, Tree.mem_pullSub_append
tree 📖	CompOp	13 math math: Tree.take_mem, Tree.mem_pullSub_long, Tree.take_coe, Tree.pullSub_adjunction, coe_def, Tree.pullSub_subAt, Tree.take_eq_take, Tree.tree_eq_bot, Tree.mem_subAt, Tree.mem_pullSub_self, Tree.mem_pullSub_short, Tree.drop_coe, Tree.mem_pullSub_append

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_def 📖	mathematical	—	SetLike.coe Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike tree instSetLikeSubtypeSetListMemCompleteSublatticeTree	—	—

Descriptive.Tree

Definitions

Name	Category	Theorems
drop 📖	CompOp	1 math math: drop_coe
instTransListSubtypeSetMemCompleteSublatticeTreeIsPrefix 📖	CompOp	—
pullSub 📖	CompOp	10 math math: pullSub_append, mem_pullSub_long, subAt_pullSub, pullSub_adjunction, pullSub_subAt, pullSub_mono, pullSub_nil, mem_pullSub_self, mem_pullSub_short, mem_pullSub_append
subAt 📖	CompOp	8 math math: subAt_pullSub, subAt_nil, subAt_mono, pullSub_adjunction, pullSub_subAt, mem_subAt, drop_coe, subAt_append
take 📖	CompOp	4 math math: take_take, take_coe, take_eq_take, drop_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
drop_coe 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree subAt take drop	—	—
mem_of_append 📖	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree	—	—	Subtype.prop
mem_of_prefix 📖	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree	—	—	mem_of_append
mem_pullSub_append 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree pullSub	—	—
mem_pullSub_long 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree pullSub	—	inf_of_le_left
mem_pullSub_self 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree pullSub	—	mem_pullSub_append
mem_pullSub_short 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree pullSub	—	—
mem_subAt 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree subAt	—	—
pullSub_adjunction 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Set.instLE pullSub subAt	—	subAt_pullSub subAt_mono le_trans pullSub_mono pullSub_subAt
pullSub_append 📖	mathematical	—	pullSub	—	CompleteSublattice.ext le_total inf_of_le_left List.IsPrefix.take mem_pullSub_short List.isPrefix_append_of_length
pullSub_mono 📖	mathematical	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Set.instLE	pullSub	—	—
pullSub_nil 📖	mathematical	—	pullSub	—	Subtype.coe_eta
pullSub_subAt 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Set.instLE pullSub subAt	—	le_total mem_of_prefix mem_pullSub_short mem_pullSub_long
singleton_mem 📖	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree	—	—	mem_of_prefix
subAt_append 📖	mathematical	—	subAt	—	CompleteSublattice.ext
subAt_mono 📖	mathematical	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Set.instLE	subAt	—	Set.preimage_mono
subAt_nil 📖	mathematical	—	subAt	—	—
subAt_pullSub 📖	mathematical	—	subAt pullSub	—	CompleteSublattice.ext
take_coe 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree take	—	—
take_eq_take 📖	mathematical	—	take Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree	—	—
take_mem 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree	—	mem_of_prefix Subtype.prop
take_take 📖	mathematical	—	take	—	—
tree_eq_bot 📖	mathematical	—	Bot.bot Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership CompleteSublattice.instSetLike Descriptive.tree CompleteSublattice.instBot Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree	—	CompleteSublattice.ext mem_of_prefix

(root)

Definitions

Name	Category	Theorems
Tree 📖	CompData	15 math math: Tree.treesOfNumNodesEq_succ, Tree.treesOfNumNodesEq_card_eq_catalan, Tree.traverse_pure, DyckWord.equivTreesOfNumNodesEq_symm_apply_coe, DyckWord.equivTreesOfNumNodesEq_apply_coe, DyckWord.equivTree_symm_apply, Tree.mem_treesOfNumNodesEq_numNodes, Tree.coe_treesOfNumNodesEq, Tree.mem_treesOfNumNodesEq, Tree.treesOfNumNodesEq_zero, Tree.instLawfulTraversable, Tree.traverse_eq_map_id, Tree.naturality, DyckWord.equivTree_apply, Tree.comp_traverse

---

← Back to Index