Commit 2025-04-06 17:49 0f50e960

View on Github →

feat: Descriptive.tree basic API (#21234) add API on Descriptive.tree, in particular operations for switching between subtrees

Estimated changes

Modified Mathlib/Data/SetLike/Basic.lean

added theorem SetLike.mem_mk

added theorem SetLike.mem_mk_set

Modified Mathlib/Order/CompleteLattice/SetLike.lean

modified theorem CompleteSublattice.mem_mk

modified theorem Sublattice.setLike_mem_mk

Modified Mathlib/SetTheory/Descriptive/Tree.lean

added def Descriptive.Tree.drop

added theorem Descriptive.Tree.mem_of_append

added theorem Descriptive.Tree.mem_of_prefix

added theorem Descriptive.Tree.mem_pullSub_append

added theorem Descriptive.Tree.mem_pullSub_long

added theorem Descriptive.Tree.mem_pullSub_self

added theorem Descriptive.Tree.mem_pullSub_short

added theorem Descriptive.Tree.mem_subAt

added def Descriptive.Tree.pullSub

added theorem Descriptive.Tree.pullSub_adjunction

added theorem Descriptive.Tree.pullSub_append

added theorem Descriptive.Tree.pullSub_mono

added theorem Descriptive.Tree.pullSub_nil

added theorem Descriptive.Tree.pullSub_subAt

added theorem Descriptive.Tree.singleton_mem

added def Descriptive.Tree.subAt

added theorem Descriptive.Tree.subAt_append

added theorem Descriptive.Tree.subAt_mono

added theorem Descriptive.Tree.subAt_nil

added theorem Descriptive.Tree.subAt_pullSub

added def Descriptive.Tree.take

added theorem Descriptive.Tree.take_eq_take

added theorem Descriptive.Tree.take_mem

added theorem Descriptive.Tree.take_take

added theorem Descriptive.Tree.tree_eq_bot

deleted theorem Descriptive.mem_of_append

deleted theorem Descriptive.mem_of_prefix

deleted theorem Descriptive.tree_eq_bot