Set.Definable.image_comp
theorem Set.Definable.image_comp :
∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {β : Type u_1}
{s : Set (β → M)},
A.Definable L s → ∀ (f : α → β) [inst_1 : Finite α] [inst_2 : Finite β], A.Definable L ((fun g => g ∘ f) '' s)
This theorem states that definability in a set is closed under finite projections. More specifically, given a type `M`, a set `A` within `M`, a first order language `L`, and a structure `inst` for the language over `M`. For any given types `α`, `β`, and a set `s` of functions from `β` to `M`, if `s` is definable in `A` with respect to `L`, then for every function `f` from `α` to `β`, assuming both `α` and `β` are finite, the image of `s` under the composition with `f` is still definable in `A` with respect to `L`. In other words, the definability property is preserved when we project `s` through some function `f` from `α` to `β`.
More concisely: Given a type `M`, a finite set `A` within `M`, a first-order language `L`, and a structure `inst` for `L` over `M`, if a set `s` of functions from a finite type `β` to `M` is definable in `A` with respect to `L`, then the composition of `s` with any finite function `f` from `α` to `β` results in a definable set in `A` with respect to `L`.
|
Set.Definable.image_comp_embedding
theorem Set.Definable.image_comp_embedding :
∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {β : Type u_1}
{s : Set (β → M)}, A.Definable L s → ∀ (f : α ↪ β) [inst_1 : Finite β], A.Definable L ((fun g => g ∘ ⇑f) '' s)
The theorem `Set.Definable.image_comp_embedding` states that the property of definability under a first-order language `L` is closed under finite projections. Specifically, given a type `M`, a set `A` of type `M`, a first-order language `L`, an `L`-structure on `M`, types `α` and `β`, and a set `s` of functions from `β` to `M` that is definable under `L`, if we have an embedding `f` from `α` to `β` and `β` is finite, then the image of `s` under the composition with `f` (i.e., the set of all functions `g` composed with `f` for `g` in `s`) is also definable under `L`.
More concisely: If `s` is a definable set of functions from a finite type `β` to a type `M`, and `f` is an embedding from type `α` to `β`, then the image of `s` under `f` is also definable.
|
Set.Definable.image_comp_sum_inl_fin
theorem Set.Definable.image_comp_sum_inl_fin :
∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} (m : ℕ)
{s : Set (α ⊕ Fin m → M)}, A.Definable L s → A.Definable L ((fun g => g ∘ Sum.inl) '' s)
This theorem, `Set.Definable.image_comp_sum_inl_fin`, states that for any type `M`, a set `A` of type `M`, a language `L` of first order logic, a structure `inst` on `M` with respect to `L`, a type `α`, a natural number `m`, and a set `s` that is a function from a sum type (`α` or `Fin m`) to `M` and is definable in `A` with respect to `L`, the image of `s` under the function composition with `Sum.inl` (which injects `α` into the sum type) is also definable in `A` with respect to `L`.
In simpler terms, it's saying that if we have a definable set of functions from a sum type to some other type, then the subset of that set which only takes elements from the left part of the sum type is also definable.
More concisely: If `s` is a definable function from a sum type to a set `A` with respect to a logic `L`, then the image of `s` under composition with `Sum.inl` is also a definable subset of `A` with respect to `L`.
|
Set.Definable.inter
theorem Set.Definable.inter :
∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {f g : Set (α → M)},
A.Definable L f → A.Definable L g → A.Definable L (f ∩ g)
The theorem `Set.Definable.inter` states that if we have two sets, `f` and `g`, which are subsets of a finite Cartesian product of a structure `M` that are definable over a set `A` with respect to a first-order language `L` (i.e., membership in both `f` and `g` can be determined by some first-order formula with parameters from `A`), then the intersection of `f` and `g` is also a set that is definable over `A` with the same first-order language `L`. This means that the set of elements common to both `f` and `g` can also be described by a first-order formula with parameters from `A`.
More concisely: If `f` and `g` are definable subsets of a finite product `M` over a set `A` with respect to a first-order language `L`, then their intersection is also a definable subset of `M` over `A` using the same language `L`.
|