Open sets are locally connected

Stream: Is there code for X?

[Vincent Beffara]

Do we have this?

theorem machin {U : Set ℂ} (hU : IsOpen U) : LocallyConnectedSpace ↑U := sorry

[Patrick Massot]

I would say yes, but that's a non-constructive proof.

[Patrick Massot]

At least we have docs#locPathConnected_of_isOpen

[Vincent Beffara]

Oh, I searched using "locally" as a substring so I didn't find this one :-( Thanks!

[Anatole Dedecker]

I don’t think we have the locally connected version though (as in the one which would only assume local connectedness of the ambient space)

[Vincent Beffara]

locally path connected says

∀ (x : ↑U), HasBasis (𝓝 x) (fun s => s ∈ 𝓝 x ∧ IsPathConnected s) id

while locally connected says

∀ (x : ↑U), HasBasis (𝓝 x) (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id

so one implication is not clear to me

[Anatole Dedecker]

We have docs#locallyConnectedSpace_iff_connected_basis

[Anatole Dedecker]

The reason it’s so far below the definition is it’s not immediate to show the equivalence

[Vincent Beffara]

But then IsPathConnected and IsConnected are not equivalent for a general neighborhood ... Anyway I have to run but I will look more into it, thanks.

[Anatole Dedecker]

Ah sorry I misunderstood. Of course they are not equivalent in general, but for you it’s in the easy direction, right?

[Vincent Beffara]

It should be, yes

[Anatole Dedecker]

#7530

[Patrick Massot]

  exact LocallyConnectedSpace.open_connected_basis (f x) |>.restrict_subset
    (h.open_range.mem_nhds <| mem_range_self _) |>.comap _

I see some people really have fun with |> and <|. It's too bad the precedences don't allow

  exact LocallyConnectedSpace.open_connected_basis (f x) |>.restrict_subset
    <| h.open_range.mem_nhds <| mem_range_self _ |>.comap _

[Vincent Beffara]

I got this which is way more pedestrian:

lemma _root_.LocPathConnectedSpace.locallyConnectedSpace (h : LocPathConnectedSpace U) :
    LocallyConnectedSpace U := by
  have h' := h.path_connected_basis
  simp only [locallyConnectedSpace_iff_connected_basis, hasBasis_iff] at h' ⊢
  intro x t ; constructor
  · intro ht
    obtain ⟨i, ⟨l1, l2⟩, l3⟩ := (h' x t).1 ht
    refine ⟨i, ⟨l1, ?_⟩, l3⟩
    rw [isPathConnected_iff_pathConnectedSpace] at l2
    exact (isConnected_iff_connectedSpace.2 l2.connectedSpace).isPreconnected
  · exact λ ⟨i, ⟨l1, _⟩, l3⟩ => Filter.mem_of_superset l1 l3

lemma _root_.IsOpen.locallyConnectedSpace (hU : IsOpen U) : LocallyConnectedSpace U := by
  exact (locPathConnected_of_isOpen hU).locallyConnectedSpace

[Anatole Dedecker]

Patrick Massot said:

  exact LocallyConnectedSpace.open_connected_basis (f x) |>.restrict_subset
    (h.open_range.mem_nhds <| mem_range_self _) |>.comap _

I see some people really have fun with |> and <|. It's too bad the precedences don't allow

  exact LocallyConnectedSpace.open_connected_basis (f x) |>.restrict_subset
    <| h.open_range.mem_nhds <| mem_range_self _ |>.comap _

That would become a bit too unreadable for my liking (but maybe I'd get used to it?) :sweat_smile: I already liked $/<|, but I'm a huge fan of |>. because it makes dot notation with extra arguments even cleaner.

[Anatole Dedecker]

Actually I'm not even sure I've ever used |> without the ., what does it do? I would guess f x y |> z = (f x y) z, but that's already what f x y z means...

[Vincent Beffara]

Apparently x |> f |> g is g (f x)

[Anatole Dedecker]

Ah that makes sense. I'm going to use it more then!

[Patrick Massot]

I fear parentheses will soon disappear from

  exact LocallyConnectedSpace.open_connected_basis (f x) |>.restrict_subset
    (h.open_range.mem_nhds <| mem_range_self _) |>.comap _

[Patrick Massot]

Unless bors is faster than Anatole.

[Anatole Dedecker]

Oh I didn't mean in this particular example. I can get rid of the parentheses by doing:

  exact .comap f <| LocallyConnectedSpace.open_connected_basis (f x) |>.restrict_subset <|
    h.open_range.mem_nhds <| mem_range_self _

But I think it looks very weird because you have no way of guessing which of .comap and .restrict_subset get applied first

[Anatole Dedecker]

Did you have something else in mind?

[Patrick Massot]

Do we have semaphore emojis?

[Patrick Massot]

And please don't push that to your PR :pray:

[Yaël Dillies]

Sorry people I still believe that the $-only world is better.

[Johan Commelin]

And you are going to propose € for the dual of $?

[Yaël Dillies]

I still don't see how the dual is supposed to work with precedence.

[Vincent Beffara]

We could use ¥ somewhere, it adds a lot of nicely confusing symmetry. Or https://www.compart.com/en/unicode/U+10197 even (apparently the quinarius was a Roman currency, and it has a nice symbol)

[Trebor Huang]

So instead of concurrency programming we now have currency programming..

[Jireh Loreaux]

@Yaël Dillies what do you mean?

[Yaël Dillies]

LIke how |> and <| associate.

[Adam Topaz]

here you go: https://github.com/leanprover/lean4/blob/b0b922bae499e6380ed3e48ad8efb25c963d5aaf/src/Init/Notation.lean#L417

[Adam Topaz]

syntax:min term " <| " term:min : term
syntax:min term " |> " term:min1 : term

[Adam Topaz]

min1 = min + 1

[Anatole Dedecker]

I would advise again making use of that precedence anyways, that makes terribly confusing terms like above. And really I think |>. is much more useful (and natural) than |>, and is in itself a good reason to use these new symbols.

[Adam Topaz]

I do think that |> can be useful. "Hey I constructed this very nice term of some type $\alpha$, but lean expects something in type $\beta$. I don't feel like moving all the way to the beginning of the line just to apply some function $f : \alpha \to \beta$, so I'll just |> f and call it a day!"

[Anatole Dedecker]

Yes I think it's useful, but dot notation already covers a lot of cases where it would be natural. That is, where we would naturally want to write x |> g |> f, we can often write x.g.f. But maybe it's just something left in my mind by Lean3.

[Adam Topaz]

That's assuming that g etc. are in the right namespace... {{a,b},{c,d}} |> Monad.join is just one example off the top of my head. Note that there is no Set.join.

[Anatole Dedecker]

Of course I'm not claiming that it covers all cases, but I've had less occasion to use it than expected thanks to dot notation.

[Adam Topaz]

Anyway, in case it's not clear, I quite like |> and <|. But now I'll stop highjacking this thread about open sets :)