theorem
proved
optimal_iff
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Core.DisplayChannel on GitHub at line 72.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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