Zulip Chat Archive

Stream: general

Topic: I don't understand heq


view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:01):

Here's a self-contained extract from analysis/topology/topological.space_lean:

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:02):

import analysis.topology.topological_space
open topological_space
universes u v w
variables {α : Type u} {β : Type v} {ι : Sort w} {a a₁ a₂ : α} {s s₁ s₂ : set α} {p p₁ p₂ : α  Prop}
variables [topological_space α]

lemma is_open_Union_orig {f : ι  set α} (h : i, is_open (f i)) : is_open (i, f i) :=
is_open_sUnion $ assume t i, (heq : t = f i), heq.symm  h i

lemma is_open_Union' {f : ι  set α} (h : i, is_open (f i)) : is_open (i, f i) :=
begin
  refine is_open_sUnion _,
  intro t,
  intro Ht,
  cases Ht with i Hi,
  exact eq.symm Hi  h i,
end

lemma is_open_Union'' {f : ι  set α} (h : i, is_open (f i)) : is_open (i, f i) :=
is_open_sUnion $ assume t i, (rfl : t = f i), eq.symm  h i -- doesn't compile

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:02):

well, the first lemma is the extract -- it's called is_open_Union in the actual file.

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:03):

I should perhaps say lemma is_open_sUnion {s : set (set α)} (h : ∀t ∈ s, is_open t) : is_open (⋃₀ s)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:03):

So I realised I didn't really understand the mathlib proof of is_open_Union_orig (which is the proof given in the extract above, with its heq)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:04):

so I proved the lemma "in the same way", in tactic mode

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:04):

and that's is_open_Union'

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:04):

and everything works fine with eq

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:05):

Oh -- got it:

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:05):

lemma is_open_Union'' {f : ι  set α} (h : i, is_open (f i)) : is_open (i, f i) :=
is_open_sUnion $ assume t i, (eq : t = f i), eq.symm  h i

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:06):

What's with this heq in the mathlib version?

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:08):

Oh!

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:08):

Got it :-)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:08):

heq has nothing to do with heq, it's just a variable name :-)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 10:09):

Oh OK, so I do understand this particular use of heq, we're calling a variable by the same name as a Lean function :-)


Last updated: May 08 2021 at 09:11 UTC