composite_setoid_iff

formal source

  52R₁ ⊗ R₂ is finer than both R₁ and R₂, so its setoid is ≤ both component setoids. -/
  53
  54/-- The composite setoid relates c₁, c₂ iff both components do. -/
  55theorem composite_setoid_iff {E₁ E₂ : Type*}
  56    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c₁ c₂ : C) :
  57    (recognizerSetoid (r₁ ⊗ r₂)).Rel c₁ c₂ ↔
  58    (recognizerSetoid r₁).Rel c₁ c₂ ∧ (recognizerSetoid r₂).Rel c₁ c₂ :=
  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₂ ∧