# Zulip Chat Archive

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

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

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