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: Dec 20 2023 at 11:08 UTC