103theorem resolutionCells_partition (c : C) : 104 ∃! cell : Set C, c ∈ cell ∧ cell = ResolutionCell r c := by
proof body
Term-mode proof.
105 use ResolutionCell r c 106 constructor 107 · exact ⟨mem_resolutionCell_self r c, rfl⟩ 108 · intro cell ⟨_, hcell⟩ 109 exact hcell 110 111/-! ## Local Resolution -/ 112 113/-- The local resolution of R at c on U is the partition of U into 114 intersections with resolution cells. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.