Zulip Chat Archive

Stream: mathlib4

Topic: ordcontinuous

Eric Rodriguez (Dec 26 2022 at 22:50):

I tried to have a look at porting this file , but failed at the first hurdle; I cannot get docs#left_ord_continuous.order_dual to compile. Is defeq way stronger in Lean4?

Eric Rodriguez (Dec 26 2022 at 22:50):

because the current id proof and variations of it using exact and convert don't seem to help

Eric Rodriguez (Dec 26 2022 at 22:50):

also to even get it to typecheck you need to ascript the statement to say OrderDual α → OrderDual β

Kevin Buzzard (Dec 26 2022 at 23:19):

protected theorem order_dual : LeftOrdContinuous f → RightOrdContinuous (toDual ∘ f ∘ ofDual) :=
  id

Kevin Buzzard (Dec 26 2022 at 23:20):

Looks like you failed to obey the golden rule for porting: set_option autoImplicit false

Kevin Buzzard (Dec 26 2022 at 23:22):

You had to ascript the statement because Lean helpfully just invented a new function to_dual from beta to some metavariable without telling you.

Kevin Buzzard (Dec 26 2022 at 23:25):

PS I would imagine that if problems start showing up with the definition of OrderDual as a type synonym then there might be a move to change it to a one field structure, and then probably proofs will start breaking :-/

Eric Rodriguez (Dec 27 2022 at 11:25):

should the theorem itself be called order_dual or orderDual, btw?

Last updated: Dec 20 2023 at 11:08 UTC