Pointwise topology

Stream: Is there code for X?

[Yaël Dillies]

Where could such a lemma go?

lemma interior_mul_interior_subset {s t : set α} :
  interior s * interior t ⊆ interior (s * t) :=

I'd say topology.pointwise but this doesn't exist yet.

[Yaël Dillies]

This comes from #10648

[Yury G. Kudryashov]

Create it?

[Yury G. Kudryashov]

topology.pointwise or topology.algebra.pointwise?

[Yury G. Kudryashov]

Note that we have docs#submonoid.top_closure_mul_self_eq in topology.algebra.monoid.

[Yaël Dillies]

Doesn't seem like a new file would do it. This stuff needs to be between lemmas about groups with continuous multiplication, and lemmas about topological groups. Both live in topology.algebra.group, so I'll land my lemmas there.

[Yaël Dillies]

While I'm at it, is the following true?

@[to_additive]
lemma closure_mul_subset : closure (s * t) ⊆ closure s * closure t  :=
closure_minimal (set.mul_subset_mul subset_closure subset_closure) $
  is_closed_closure.mul is_closed_closure

For it to work, I need that the multiplication of closed sets is a closed set, which sounds reasonable but I can't think of a proof.

[Yaël Dillies]

Ah nope it's wrong. Thanks Analysis & Topology Example Sheet 3.

[Alex J. Best]

Which way round are you asking about/

[Alex J. Best]

closure (s * t) ⊆ closure s * closure t ⊆ closure (s * t) doesn't look like lean will be happy to me

[Yaël Dillies]

Ahah oops. I was being indecise.

[Yaël Dillies]

The counterexample is ((λ x, x + 1/x) '' {n : ℕ | 0 < n}) + ((λ x, -x) '' (univ : set ℕ)).