`refl`

proved

show as: view math explainer →

module: IndisputableMonolith.RRF.Core.DisplayChannel
domain: RRF
line: 58 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RRF.Core.DisplayChannel on GitHub at line 58.

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

formal source

  55
  56variable {State Obs₁ Obs₂ Obs₃ : Type*}
  57
  58theorem refl (C : DisplayChannel State Obs₁) : QualityEquiv C C :=
  59  fun _ _ => Iff.rfl
  60
  61theorem symm {C₁ : DisplayChannel State Obs₁} {C₂ : DisplayChannel State Obs₂}
  62    (h : QualityEquiv C₁ C₂) : QualityEquiv C₂ C₁ :=
  63  fun x y => (h x y).symm
  64
  65theorem trans {C₁ : DisplayChannel State Obs₁}
  66    {C₂ : DisplayChannel State Obs₂}
  67    {C₃ : DisplayChannel State Obs₃}
  68    (h₁₂ : QualityEquiv C₁ C₂) (h₂₃ : QualityEquiv C₂ C₃) : QualityEquiv C₁ C₃ :=
  69  fun x y => (h₁₂ x y).trans (h₂₃ x y)
  70
  71/-- Quality-equivalent channels have the same optimal states. -/
  72theorem optimal_iff {C₁ : DisplayChannel State Obs₁} {C₂ : DisplayChannel State Obs₂}
  73    (heq : QualityEquiv C₁ C₂) (x : State) :
  74    C₁.isOptimal x ↔ C₂.isOptimal x :=
  75  ⟨fun h1 y => (heq x y).mp (h1 y), fun h2 y => (heq x y).mpr (h2 y)⟩
  76
  77end QualityEquiv
  78
  79end RRF.Core
  80end IndisputableMonolith

papers checked against this theorem

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