OAI/Probability/FirstPassage/SeparatedSelection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PlanarFPP.separated_selection line 8

    Also declared: OAI/Probability/GammaPassage/OrientedSelection.lean:23 (same declaration text).

  2. def OAI.PlanarFPP.latticeNear line 51

    Also declared: OAI/Probability/GammaPassage/OrientedSelection.lean:66 (same declaration text).

  3. instance OAI.PlanarFPP.(instance at line 54) line 54
  4. theorem OAI.PlanarFPP.latticeNear_refl line 57

    Also declared: OAI/Probability/GammaPassage/OrientedSelection.lean:72 (same declaration text).

  5. theorem OAI.PlanarFPP.latticeNear_symm line 60

    Also declared: OAI/Probability/GammaPassage/OrientedSelection.lean:75 (same declaration text).

  6. theorem OAI.PlanarFPP.near_filter_card_le line 65

    Distinct definitions of this name: OAI/Probability/GammaPassage/OrientedSelection.lean:80 (same statement text; different proof or body). Qualify references as OAI.PlanarFPP.near_filter_card_le@path.

  7. theorem OAI.PlanarFPP.lattice_separated_selection line 77

    Also declared: OAI/Probability/GammaPassage/OrientedSelection.lean:94 (same declaration text).