## Stream: general

### Topic: I don't understand heq

#### Kevin Buzzard (Apr 14 2018 at 10:01):

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

#### 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


#### 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.

#### 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)

#### 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)

#### Kevin Buzzard (Apr 14 2018 at 10:04):

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

#### Kevin Buzzard (Apr 14 2018 at 10:04):

and that's is_open_Union'

#### Kevin Buzzard (Apr 14 2018 at 10:04):

and everything works fine with eq

Oh -- got it:

#### 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


#### Kevin Buzzard (Apr 14 2018 at 10:06):

What's with this heq in the mathlib version?

Oh!

Got it :-)

#### Kevin Buzzard (Apr 14 2018 at 10:08):

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

#### 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