theorem proved term proof

`composite_cell_subset_left`

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

formal statement (Lean)

 101theorem composite_cell_subset_left (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
 102    ResolutionCell (r₁ ⊗ r₂) c ⊆ ResolutionCell r₁ c := by

proof body

Term-mode proof.

 103  rw [composite_resolutionCell]
 104  exact Set.inter_subset_left
 105

depends on (2)

Lean names referenced from this declaration's body.

composite_resolutionCell in IndisputableMonolith.RecogGeom.Composition decl_use
ResolutionCell in IndisputableMonolith.RecogGeom.Indistinguishable decl_use