Constant functions

This file defines Function.IsConst, the predicate that a function takes the same value at every pair of inputs.

Note that a function with empty domain is considered constant. If a constant function has non-empty codomain, then it can be represented by Function.const, see isConst_iff_exists_eq_const.

def Function.IsConst {α : Sort u_1} {β : Sort u_2} (f : α → β) : Prop

A function is constant if it takes equal values at any two inputs.

Note that a function with empty domain is considered constant. If a constant function has non-empty co domain, then it can be represented by Function.const, see isConst_iff_exists_eq_const.

The intended use is for expressing that a function is constant when the exact constant value is not known, not unique or not easy to express. To state the constant value explicitly, use Function.const.

theorem Function.isConst_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} : IsConst f ↔ ∀ (x y : α), f x = f y

theorem Function.IsConst.eq {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : IsConst f) (x y : α) : f x = f y

@[simp]

theorem Function.IsConst.const {α : Sort u_1} {β : Sort u_2} (b : β) : IsConst (const α b)

@[simp]

theorem Function.IsConst.of_subsingleton_domain {α : Sort u_1} {β : Sort u_2} [Subsingleton α] (f : α → β) : IsConst f

All function on a subsingleton domain are constant.

@[simp]

theorem Function.IsConst.of_subsingleton_codomain {α : Sort u_1} {β : Sort u_2} [Subsingleton β] (f : α → β) : IsConst f

All function to a subsingleton codomain are constant.

theorem Function.IsConst.of_forall_eq {α : Sort u_1} {β : Sort u_2} {f : α → β} (b : β) (h : ∀ (x : α), f x = b) : IsConst f

theorem Function.isConst_iff_exists_forall_eq {α : Sort u_1} {β : Sort u_2} [Nonempty β] {f : α → β} : IsConst f ↔ ∃ (b : β), ∀ (x : α), f x = b

A function f : α → β is constant on a non-empty codomain if and only if there is b : β so that f a = b for all a : α.

theorem Function.isConst_iff_exists_forall_eq_of_nonempty_domain {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} : IsConst f ↔ ∃ (b : β), ∀ (x : α), f x = b

A function f : α → β is constant on a non-empty domain if and only if there is b : β so that f a = b for all a : α.

theorem Function.isConst_iff_exists_eq_const {α : Sort u_1} {β : Sort u_2} [Nonempty β] {f : α → β} : IsConst f ↔ ∃ (b : β), f = const α b

A function α → β is constant on a non-empty codomain if and only if there is b : β so that the function can be written as Function.const α b.

theorem Function.IsConst.exists_eq_const {α : Sort u_1} {β : Sort u_2} [Nonempty β] {f : α → β} : IsConst f → ∃ (b : β), f = const α b

Alias of the forward direction of Function.isConst_iff_exists_eq_const.

---

A function α → β is constant on a non-empty codomain if and only if there is b : β so that the function can be written as Function.const α b.

theorem Function.isConst_iff_exists_eq_const_of_nonempty_domain {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} : IsConst f ↔ ∃ (b : β), f = const α b

A function α → β is constant on a non-empty domain if and only if there is b : β so that the function can be written as Function.const α b.

theorem Function.IsConst.comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : IsConst f) (g : β → γ) : IsConst (g ∘ f)

Postcomposition preserves being constant.

theorem Function.IsConst.comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : β → γ} (hg : IsConst g) (f : α → β) : IsConst (g ∘ f)

Precomposing a constant function gives a constant function.

theorem Function.not_isConst_of_apply_ne {α : Sort u_1} {β : Sort u_2} {f : α → β} {x y : α} (h : f x ≠ f y) : ¬IsConst f

theorem Function.not_isConst_iff_exists_apply_ne {α : Sort u_1} {β : Sort u_2} {f : α → β} : ¬IsConst f ↔ ∃ (x : α) (y : α), f x ≠ f y

@[simp]

theorem Function.isConst_id_iff {α : Sort u_1} : IsConst id ↔ Subsingleton α

The identity function on a type is constant if and only if the type is a subsingleton.

@[simp]

theorem Setoid.ker_eq_top {α : Type u_4} {β : Type u_5} {f : α → β} : ker f = ⊤ ↔ Function.IsConst f

@[simp]

theorem Set.subsingleton_range_iff {α : Sort u_1} {β : Type u_4} {f : α → β} : (range f).Subsingleton ↔ Function.IsConst f

@[simp]

theorem Set.nontrivial_range_iff {α : Sort u_1} {β : Type u_4} {f : α → β} : (range f).Nontrivial ↔ ¬Function.IsConst f

theorem Function.isConst_and_injective_iff {α : Sort u_1} {β : Sort u_2} (f : α → β) : IsConst f ∧ Injective f ↔ Subsingleton α

theorem Function.IsConst.injective_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (h : IsConst f) : Injective f ↔ Subsingleton α

theorem Function.Injective.isConst_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (h : Injective f) : IsConst f ↔ Subsingleton α

theorem Function.isConst_and_surjective_iff {α : Sort u_1} {β : Sort u_2} (f : α → β) : IsConst f ∧ Surjective f ↔ IsEmpty β ∨ Nonempty α ∧ Subsingleton β

theorem Function.isConst_and_surjective_iff_of_nonempty {α : Sort u_1} {β : Sort u_2} [Nonempty α] (f : α → β) : IsConst f ∧ Surjective f ↔ Subsingleton β

theorem Function.IsConst.surjective_iff {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} (h : IsConst f) : Surjective f ↔ Subsingleton β

theorem Function.Surjective.isConst_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (h : Surjective f) : IsConst f ↔ Subsingleton β