Frame implies HeytingAlgebra

Stream: Is there code for X?

[Floris van Doorn]

I believe this is missing in Mathlib?

import Mathlib

example {α : Type*} [Order.Frame α] : HeytingAlgebra α := by sorry

( @Yaël Dillies mentioned in another thread that he was planning to let Frame extend HeytingAlgebra)

[Eric Wieser]

I think there is a PR from @Yaël Dillies already

[Floris van Doorn]

Oh yes, #10560

[Yaël Dillies]

Yes, that's right. But currently I'm waiting for @Eric Wieser to review #12731 :grinning: