`composite_resolutionCell`

proved

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.Composition
domain: RecogGeom
line: 94 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RecogGeom.Composition on GitHub at line 94.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  91/-! ## Resolution Cell Refinement -/
  92
  93/-- Resolution cells under composite are intersections of component cells -/
  94theorem composite_resolutionCell (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
  95    ResolutionCell (r₁ ⊗ r₂) c = ResolutionCell r₁ c ∩ ResolutionCell r₂ c := by
  96  ext c'
  97  simp only [ResolutionCell, Set.mem_setOf_eq, Set.mem_inter_iff,
  98             composite_indistinguishable_iff]
  99
 100/-- Composite resolution cells are subsets of either component cell -/
 101theorem composite_cell_subset_left (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
 102    ResolutionCell (r₁ ⊗ r₂) c ⊆ ResolutionCell r₁ c := by
 103  rw [composite_resolutionCell]
 104  exact Set.inter_subset_left
 105
 106theorem composite_cell_subset_right (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
 107    ResolutionCell (r₁ ⊗ r₂) c ⊆ ResolutionCell r₂ c := by
 108  rw [composite_resolutionCell]
 109  exact Set.inter_subset_right
 110
 111/-! ## Quotient Maps -/
 112
 113/-- There is a natural map from the composite quotient to the r₁ quotient -/
 114def quotientMapLeft (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 115    RecognitionQuotient (r₁ ⊗ r₂) → RecognitionQuotient r₁ :=
 116  Quotient.lift (recognitionQuotientMk r₁) (fun c₁ c₂ h =>
 117    (quotientMk_eq_iff r₁).mpr (composite_refines_left r₁ r₂ h))
 118
 119/-- There is a natural map from the composite quotient to the r₂ quotient -/
 120def quotientMapRight (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 121    RecognitionQuotient (r₁ ⊗ r₂) → RecognitionQuotient r₂ :=
 122  Quotient.lift (recognitionQuotientMk r₂) (fun c₁ c₂ h =>
 123    (quotientMk_eq_iff r₂).mpr (composite_refines_right r₁ r₂ h))
 124

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.