OAI/MathematicalPhysics/Boltzmann/Branching/FanNullSet.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Nullity of a set whose lines through one point have null sections

  1. abbrev OAI.BoltzmannNonuniqueness.Published.FanRemainder line 13
  2. abbrev OAI.BoltzmannNonuniqueness.Published.FanPhase line 14
  3. def OAI.BoltzmannNonuniqueness.Published.fan line 16
  4. theorem OAI.BoltzmannNonuniqueness.Published.fan_null_set line 19