working with sigma-compact spaces - stuck at syntax

Stream: new members

[Michael Rothgang]

Hi! Given a $\sigma$-compact topological space, I'm trying to extract the covering by compacts from it --- but am stuck. (I found the items in the documentation, but everything I tried was invalid syntax...) Pretty sure I'm just missing a trick. Advice would be welcome.

import Mathlib.MeasureTheory.Measure.Hausdorff
import Mathlib.Topology.MetricSpace.Lipschitz
lemma dummy { X Y : Type }
    [MetricSpace X] [SigmaCompactSpace X] [MetricSpace Y] { d : ℕ } : True := by
  -- Choose a cover of X by compact sets K_i.
  -- Question: fill in the sorries: how to use these theorems?
  let cov : ℕ → Set X := sorry -- mumble mumble SigmaCompactSpace.compact_covering X
  have hcov : ⋃ (n : ℕ), cov n = Set.univ := by sorry -- mumble mumble iUnion_compactCovering
  have hcompact : ∀ n : ℕ, IsCompact (cov n) := by sorry -- mumble mumble isCompact_compactCovering
  sorry

[Michael Rothgang]

Meta: it seems LaTeX in the topic name doesn't work? Ok, point taken.

[Anatole Dedecker]

Yes you can't do LaTeX in the title

[Anatole Dedecker]

This works:

import Mathlib.MeasureTheory.Measure.Hausdorff
import Mathlib.Topology.MetricSpace.Lipschitz

lemma dummy { X Y : Type }
    [MetricSpace X] [SigmaCompactSpace X] [MetricSpace Y] { d : ℕ } : True := by
  -- Choose a cover of X by compact sets K_i.
  -- Question: fill in the sorries: how to use these theorems?
  let cov : ℕ → Set X := compactCovering X
  have hcov : ⋃ (n : ℕ), cov n = Set.univ := iUnion_compactCovering X
  have hcompact : ∀ n : ℕ, IsCompact (cov n) := isCompact_compactCovering X
  sorry

[Anatole Dedecker]

For the first one, note that docs#compactCovering is (perhaps surprisingly) not called SigmaCompactSpace.compactCovering

[Anatole Dedecker]

For the second and third ones, you have to specify the right amount of explicit arguments (or you could also do by apply iUnion_compactCovering, which inserts arguments if needed)

[Damiano Testa]

There is also the .. syntax that includes the right number of trailing _.

[Anatole Dedecker]

Oh that's a nice trick, I did not know about that

[Anatole Dedecker]

Michael, do you know the distinction between tactic mode and term mode? I'm asking since you mentioned syntax errors, and by the look of your code I was wondering wether you were trying to mix the two

[Michael Rothgang]

Anatole Dedecker said:

Michael, do you know the distinction between tactic mode and term mode? I'm asking since you mentioned syntax errors, and by the look of your code I was wondering wether you were trying to mix the two

I do! I know sorry can act both as a proof term and as a tactic. :-)

[Michael Rothgang]

Anatole Dedecker said:

For the first one, note that docs#compactCovering is (perhaps surprisingly) not called SigmaCompactSpace.compactCovering

Thanks, that helps. I guess I was confused by the description in the docstring: "The sequence can be extracted using topological_space.compact_covering." I interpreted, guessing, this as some expression X.compact_covering - I presume that was a typo instead and should read TopologicalSpace.compactCovering instead?

[Ruben Van de Velde]

That sounds like an accidental leftover from lean 3; can you link to the place where you read that?

[Kevin Buzzard]

This also looks wrong -- topological_space is Lean 3 speak.

[Patrick Massot]

Docstrings mentioning declaration are tricky. They were easy to miss while porting.

[Anatole Dedecker]

Fixed in #7065

[Anatole Dedecker]

"The sequence can be extracted using topological_space.compact_covering." I interpreted, guessing, this as some expression X.compact_covering - I presume that was a typo instead and should read TopologicalSpace.compactCovering instead?

Not quite: the right name is just compactCovering with no namespace (and it wasn't in a namespace in Lean3 either, so the docstring was already wrong). Besides, not all lemmas in a namespace can be used with dot notation, sometimes it's just a matter of organizing lemmas. So you wouldn't have been able to do X.compactCovering anyways. Note that dot notation is a very handy feature but it's never necessary, so if you are fighting syntax errors you should try referring to lemmas by their full name and not use dot notation.

[Michael Rothgang]

Thanks for the advice, I'll keep that in mind.