theorem proved term proof

`box_phase_hit_gives_repr`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  67theorem box_phase_hit_gives_repr {n c : ℕ}
  68    (h : HitsBalancedPhase n c) :
  69    ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=

proof body

Term-mode proof.

  70  balanced_pair_phase_support_gives_repr (box_phase_hit_gives_balanced_pair h)
  71
  72end ErdosStrausBoxPhase
  73end NumberTheory
  74end IndisputableMonolith

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

box_phase_hit_gives_repr_logic in IndisputableMonolith.NumberTheory.LogicErdosStrausBoxPhase decl_use
generated_phase_hit_gives_repr in IndisputableMonolith.NumberTheory.SubsetProductPhase decl_use

depends on (4)

Lean names referenced from this declaration's body.

box_phase_hit_gives_balanced_pair in IndisputableMonolith.NumberTheory.ErdosStrausBoxPhase decl_use
HitsBalancedPhase in IndisputableMonolith.NumberTheory.ErdosStrausBoxPhase decl_use
HasRationalErdosStrausRepr in IndisputableMonolith.NumberTheory.ErdosStrausRCL decl_use
balanced_pair_phase_support_gives_repr in IndisputableMonolith.NumberTheory.ErdosStrausRotationHierarchy decl_use