continuous_of_const

Stream: maths

[Patrick Massot]

This is very much related to my question in the https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/Empty.20or.20not.20empty/near/152017713, but has some (tiny) math content. Can anyone golf the following ridiculous lemma?

lemma continuous_of_const {α : Type*} {β : Type*} [topological_space α] [topological_space β] {f : α → β} (h : ∀a b, f a = f b) :
  continuous f :=
begin
  by_cases H : ∃ x : α, true,
  { cases H with a,
    rw show f = λ x, f a, by ext x; rw h,
    exact continuous_const },
  { intros U Uin,
    convert is_open_empty,
    rw set.eq_empty_iff_forall_not_mem,
    intro x,
    exfalso,
    exact H ⟨x, trivial⟩ }
end

@Kenny, can you can rid of axiom of choice here? I don't even know where it crops in.

[Patrick Massot]

Of course you need to import analysis.topology.topological_space

[Kenny Lau]

I don't think I can do much regarding axiom of choice

[Kenny Lau]

import analysis.topology.continuity

lemma continuous_of_const {α : Type*} {β : Type*} [topological_space α] [topological_space β] {f : α → β} (h : ∀a b, f a = f b) :
  continuous f :=
λ s _, classical.by_cases
  (λ hs : f ⁻¹' s = ∅, hs.symm ▸ is_open_empty)
  (λ hs : f ⁻¹' s ≠ ∅, let ⟨y, hy⟩ := set.exists_mem_of_ne_empty hs in
    have set.univ = f ⁻¹' s, from eq.symm $ set.eq_univ_of_forall $ λ x,
      show f x ∈ s, from h y x ▸ hy,
    this ▸ is_open_univ)

[Patrick Massot]

Nice effort, but it doesn't change much (about the same length, same axioms)

[Mario Carneiro]

isn't there a lemma that says a constant proposition is open?

[Mario Carneiro]

is_open_const

[Kenny Lau]

but this is a different formulation of "constant"

[Mario Carneiro]

right, but it is the one you want here, I think

[Mario Carneiro]

it doesn't avoid LEM (because it's used in the proof) but you can defer the case splitting to it

[Mario Carneiro]

lemma continuous_of_const {α : Type*} {β : Type*}
  [topological_space α] [topological_space β]
  {f : α → β} (h : ∀a b, f a = f b) :
  continuous f :=
λ s _, by convert @is_open_const _ _ (∃ a, f a ∈ s); exact
  set.ext (λ a, ⟨λ fa, ⟨_, fa⟩,
    λ ⟨b, fb⟩, show f a ∈ s, from h b a ▸ fb⟩)

[Kenny Lau]

nice

[Patrick Massot]

I have a long way to go before becoming a true obfuscation master...

[Patrick Massot]

Thanks anyway!