OAI/Analysis/LipschitzHilbert/Trees/SourceOrdinaryTreeIdentity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The original selected tree is exactly its short part, the frozen long part, and the long selector error, all on one Whitney partition.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.ordinary_tree_split_identity line 16