Theorems · Theorem · logic and foundations

Set.DefinableFun.setOf_eq_const

Deprecated since 2026-07-09Use Set.DefinableFun.ofPred_eq_const instead.

∀ {M : Type u_1} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u_2} {A : Set M} {f : (α → M) → M},
  Set.DefinableFun L A f → ∀ {a : M}, a ∈ A → A.Definable L {v | f v = a}

Alias of Set.DefinableFun.ofPred_eq_const. The preimage of a constant under a definable function is definable.

Defined in

Mathlib.ModelTheory.Definability

Cited by

0 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.Structure