instance inheritance

Stream: new members

[Roberto Alvarez]

I'm trying to get a topological_space instance on a structure extending continuous functions, how do I get the induced compact-open topology?

structure X extends C(α,β) := (prop : ...  )
instance X.top :  topological_space X :=   ...   @continuous_map.compact_open α β  _ _,

[Eric Wieser]

docs#topological_space.induced?

[Eric Wieser]

With X.to_continuous_function or whatever the name of C(α,β) is

[Junyan Xu]

Oh if you make it a subtype it will automatically get docs#subtype.topological_space (which is defined using topological_space.induced), and I don't see any special benefit of naming the boundary field ...

[Roberto Alvarez]

Thanks! This does the trick:

instance X.top :  topological_space X :=
exact topological_space.induced (X.to_continuous_map) continuous_map.compact_open,

[Junyan Xu]

And doesn't C(α,β) automatically get the docs#continuous_map.compact_open instance?

[Roberto Alvarez]

I don't know how to check it

[Junyan Xu]

in this case exact topological_space.induced (X.to_continuous_map) (by apply_instance) works if the instance on C(α,β) can be inferred, and using by show_term { apply_instance } you should be able to see what instance you actually get. (Indeed it's the compact-open.)

[Roberto Alvarez]

Cool! Thanks

[rambip]

Hi !!!
I'm struggling with a very simple proof, could someone help me ?

theorem t: ∀ x y a: Nat, (x+a = y+a) -> (x = y)

I would like to do it by contradiction but I don't know how to do it ...

[Julian Berman]

Hello @rambip -- probably a bit better to ask this in a new topic, you can do that by changing the thing after the > just above where you typed your message next time. (Someone may move your message so don't worry about it now).

As for your question -- this theorem is in lean core actually, it's Nat.add_right_cancel, so you can do theorem t: ∀ x y a: Nat, (x+a = y+a) -> (x = y) := λ _ _ _ => Nat.add_right_cancel for a term mode proof, or if you are learning some basic tactics, the spelling is:

theorem t: ∀ x y a: Nat, (x+a = y+a) -> (x = y) := by
  intro x y a
  exact Nat.add_right_cancel