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

localResolution_covers

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)

 119theorem localResolution_covers (U : Set C) :
 120    ⋃₀ LocalResolution r U = U := by

proof body

Term-mode proof.

 121  ext c
 122  simp only [Set.mem_sUnion, LocalResolution, Set.mem_setOf_eq]
 123  constructor
 124  · intro ⟨S, ⟨c', hc'U, hS⟩, hcS⟩
 125    rw [hS] at hcS
 126    exact hcS.1
 127  · intro hcU
 128    refine ⟨U ∩ ResolutionCell r c, ⟨c, hcU, rfl⟩, ?_⟩
 129    exact ⟨hcU, mem_resolutionCell_self r c⟩
 130
 131/-! ## Distinguishability -/
 132
 133/-- Two configurations are distinguishable if they produce different events -/

depends on (7)

Lean names referenced from this declaration's body.