pith. machine review for the scientific record. sign in
theorem proved term proof

subsetProductPhaseHit_of_hitsBalancedPhase

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  72theorem subsetProductPhaseHit_of_hitsBalancedPhase {n c : ℕ}
  73    (h : HitsBalancedPhase n c) :
  74    Nonempty (SubsetProductPhaseHit n c) := by

proof body

Term-mode proof.

  75  rcases h with ⟨x, N, box, hn, hc, hx, hNpos, hN, hcdef, hdvd, hevd⟩
  76  refine ⟨SubsetProductPhaseHit.mk x N box hn hc hx hNpos hN hcdef hdvd hevd⟩
  77
  78/-- The two formulations are equivalent. -/

used by (2)

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

depends on (5)

Lean names referenced from this declaration's body.