OAI/Computability/DepthThree/SparseFiniteFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DepthThreeLowerBound.sparseMinimalFamily line 12
2. theorem OAI.DepthThreeLowerBound.mem_sparseMinimalFamily line 16
3. theorem OAI.DepthThreeLowerBound.sparseMinimalFamily_subset line 21
4. theorem OAI.DepthThreeLowerBound.sparseMinimalFamily_antichain line 26
5. theorem OAI.DepthThreeLowerBound.exists_mem_sparseMinimalFamily_subset line 33
6. theorem OAI.DepthThreeLowerBound.forall_sparseMinimalFamily_iff line 51
7. theorem OAI.DepthThreeLowerBound.sparseMinimalFamily_empty line 62