desc — Mathlib

English

If g ∘ f is locally constant and g is injective, then f is locally constant.

Русский

Если g ∘ f локально константна и g инъективна, тогда f локально константна.

LaTeX

$$IsLocallyConstant f$$

Lean4

/-- If a composition of a function `f` followed by an injection `g` is locally
constant, then the locally constant property descends to `f`. -/
theorem desc {α β : Type*} (f : X → α) (g : α → β) (h : IsLocallyConstant (g ∘ f)) (inj : Function.Injective g) :
    IsLocallyConstant f := fun s =>
  by
  rw [← preimage_image_eq s inj, preimage_preimage]
  exact h (g '' s)

Похожие утверждения