locally_constant_on

Stream: Is there code for X?

[Kalle Kytölä]

I have two "human powered library search" questions about locally constant functions on connected spaces/sets.

[Kalle Kytölä]

(1) I could not locate the following triviality. Is it not in mathlib, and if not, why?

import topology.locally_constant.basic
import topology.continuous_function.basic

open topological_space set
open_locale topological_space

lemma is_locally_constant.is_constant_of_connected_space {X Y : Type*}
  [topological_space X] [connected_space X]
  (f : X → Y) (f_loc_cst : is_locally_constant f) :
  ∀ x y, f x = f y :=
begin
  intros x x₀,
  by_contradiction con,
  set U := {z : X | f z = f x₀} with U_def,
  have U_open : is_open U, from is_locally_constant.is_open_fiber f_loc_cst (f x₀),
  have Uc_open : is_open Uᶜ,
    by simp only [is_locally_constant.is_closed_fiber f_loc_cst (f x₀), is_open_compl_iff],
  have U_nonemp : U.nonempty, from ⟨x₀, by simp only [mem_set_of_eq]⟩,
  have Uc_nonemp : Uᶜ.nonempty,
    from ⟨x, by simp only [mem_set_of_eq, con, mem_compl_eq, not_false_iff]⟩,
  have := ‹connected_space X›.is_preconnected_univ,
  simpa using this U Uᶜ U_open Uc_open (by simp only [union_compl_self])
    (by simp only [U_nonemp, univ_inter]) (by simp only [Uc_nonemp, univ_inter]),
end

[Kalle Kytölä]

(2) What is the canonical spelling of "being locally constant on a set"? I guessis_locally_constant (subtype.restrict A f) for (f : X → Y) (A : set X) is one clumsy spelling... I expected to find docs#is_locally_constant_on, but didn't. Presumably typically one would, for example, like to conclude something like the above is_locally_constant.is_constant_of_connected_space but on a connected subset $A \subseteq X$, i.e., have a similar lemma is_locally_constant.is_constant_of_is_connected.

[Alex J. Best]

For 1 docs#is_locally_constant.apply_eq_of_is_preconnected is fairly close but probably docs#is_locally_constant.apply_eq_of_preconnected_space should be added too

[Kalle Kytölä]

Thanks! I like the fact that docs#is_locally_constant.apply_eq_of_is_preconnected is on sets. But the good assumption should be locally constantness of the function on that set, right?

[Kalle Kytölä]

In other words, isn't it too restrictive to require locally constantness everywhere by is_locally_constant? This is why I wanted is_locally_constant_on.

[Alex J. Best]

To me that certainly sounds like a useful notion, and I can't find it anywhere either, I guess just nobody needed it so far?