composite_setoid_le_left

formal source

  59  composite_indistinguishable_iff r₁ r₂ c₁ c₂
  60
  61/-- **Refinement Left**: The composite setoid is at least as fine as r₁'s. -/
  62theorem composite_setoid_le_left {E₁ E₂ : Type*}
  63    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
  64    recognizerSetoid (r₁ ⊗ r₂) ≤ recognizerSetoid r₁ :=
  65  fun h => ((composite_setoid_iff r₁ r₂ _ _).mp h).1
  66
  67/-- **Refinement Right**: The composite setoid is at least as fine as r₂'s. -/
  68theorem composite_setoid_le_right {E₁ E₂ : Type*}
  69    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
  70    recognizerSetoid (r₁ ⊗ r₂) ≤ recognizerSetoid r₂ :=
  71  fun h => ((composite_setoid_iff r₁ r₂ _ _).mp h).2
  72
  73/-! ## Section 3: The Infimum (Meet) Property
  74
  75The composite setoid is the greatest lower bound (infimum) of the two
  76component setoids in the lattice of setoids on C. -/
  77
  78/-- **Infimum Property**: The composite setoid is the greatest setoid
  79    that is at least as fine as both r₁ and r₂. -/
  80theorem composite_setoid_is_inf {E₁ E₂ : Type*}
  81    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
  82    -- (1) composite ≤ r₁
  83    recognizerSetoid (r₁ ⊗ r₂) ≤ recognizerSetoid r₁ ∧
  84    -- (2) composite ≤ r₂
  85    recognizerSetoid (r₁ ⊗ r₂) ≤ recognizerSetoid r₂ ∧
  86    -- (3) greatest: any s ≤ r₁ and s ≤ r₂ implies s ≤ composite
  87    ∀ (s : Setoid C), s ≤ recognizerSetoid r₁ → s ≤ recognizerSetoid r₂ →
  88      s ≤ recognizerSetoid (r₁ ⊗ r₂) := by
  89  refine ⟨composite_setoid_le_left r₁ r₂, composite_setoid_le_right r₁ r₂, ?_⟩
  90  intro s h₁ h₂ hs
  91  exact (composite_setoid_iff r₁ r₂ _ _).mpr ⟨h₁ hs, h₂ hs⟩
  92