OAI/Geometry/CylinderCovering/Rational/RationalThresholdSource.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SlopeRational.ThresholdSource.actual_inverse_expansions line 11
2. theorem OAI.SlopeRational.ThresholdSource.labelDomain_subset_rectangle line 91
3. theorem OAI.SlopeRational.ThresholdSource.actual_threshold_unique line 100
4. theorem OAI.SlopeRational.ThresholdSource.fixed_quadratic_threshold_unique line 123
5. theorem OAI.SlopeRational.ThresholdSource.fixed_quadratic_sweep_coverage line 141