# Zulip Chat Archive

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

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

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?

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

Oh!

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

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