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

resolutionCell_eq_iff

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)

  85theorem resolutionCell_eq_iff {c₁ c₂ : C} :
  86    ResolutionCell r c₁ = ResolutionCell r c₂ ↔ c₁ ~[r] c₂ := by

proof body

Tactic-mode proof.

  87  constructor
  88  · intro h
  89    have : c₂ ∈ ResolutionCell r c₁ := by
  90      rw [h]
  91      exact mem_resolutionCell_self r c₂
  92    exact (Indistinguishable.symm' r this)
  93  · intro h
  94    ext c
  95    simp [ResolutionCell, Indistinguishable]
  96    constructor
  97    · intro hc
  98      exact Eq.trans hc h
  99    · intro hc
 100      exact Eq.trans hc (Eq.symm h)
 101
 102/-- Resolution cells partition the configuration space -/

depends on (6)

Lean names referenced from this declaration's body.