## Stream: maths

### Topic: continuous_of_const

#### Patrick Massot (Dec 17 2018 at 10:34):

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 (Dec 17 2018 at 10:35):

Of course you need to import analysis.topology.topological_space

#### Kenny Lau (Dec 17 2018 at 10:43):

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

#### Kenny Lau (Dec 17 2018 at 10:52):

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 (Dec 17 2018 at 10:57):

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

#### Mario Carneiro (Dec 17 2018 at 10:59):

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

#### Mario Carneiro (Dec 17 2018 at 10:59):

is_open_const

#### Kenny Lau (Dec 17 2018 at 11:00):

but this is a different formulation of "constant"

#### Mario Carneiro (Dec 17 2018 at 11:00):

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

#### Mario Carneiro (Dec 17 2018 at 11:01):

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

#### Mario Carneiro (Dec 17 2018 at 11:07):

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⟩)


nice

#### Patrick Massot (Dec 17 2018 at 11:09):

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

#### Patrick Massot (Dec 17 2018 at 11:10):

Thanks anyway!

Last updated: May 18 2021 at 08:14 UTC