Mathlib.ModelTheory.Order._auxLemma.7
theorem Mathlib.ModelTheory.Order._auxLemma.7 :
∀ {α : Sort u_1} {p : α → Prop} {a' : α}, (∀ (a : α), a = a' → p a) = p a'
This theorem, named `Mathlib.ModelTheory.Order._auxLemma.7`, states that for any type `α`, any proposition `p` that applies to items of type `α`, and any item `a'` of type `α`, if `p` is true for all items `a` that are equal to `a'`, then `p` is also true for `a'`. In other words, if we know that a property `p` holds for all elements equal to a given element `a'`, we can directly infer that this property holds for `a'` itself.
More concisely: If `p` is a proposition that holds for all equal elements `a` of type `α`, then `p` holds for `a'`.
|
Mathlib.ModelTheory.Order._auxLemma.3
theorem Mathlib.ModelTheory.Order._auxLemma.3 :
∀ {α : Type u} {x a : α} {s : Set α}, (x ∈ insert a s) = (x = a ∨ x ∈ s)
The theorem `Mathlib.ModelTheory.Order._auxLemma.3` states that for any type `α`, any elements `x` and `a` of this type, and any set `s` of `α`, the membership of `x` in the set achieved by inserting `a` into `s` is equivalent to `x` being equal to `a` or `x` being a member of `s`. Essentially, it expresses the property of set insertion in the context of set membership: an element belongs to an extended set if and only if it is either the new element inserted or an element of the original set.
More concisely: For any set `s` and elements `x` and `a` in a type `α`, `x ∈ s.insert a` if and only if `x = a` or `x ∈ s`.
|
Mathlib.ModelTheory.Order._auxLemma.16
theorem Mathlib.ModelTheory.Order._auxLemma.16 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ}
{θ : L.BoundedFormula α l.succ} {v : α → M} {xs : Fin l → M},
θ.ex.Realize v xs = ∃ a, θ.Realize v (Fin.snoc xs a)
This theorem states that for any first order language `L`, type `M` that is a structure for `L`, another type `α`, a natural number `l`, a bounded formula `θ` in `L` with `α` and `l+1` parameters, a function from `α` to `M`, and a function from the finite ordinal number `l` to `M`, the realization of the bounded formula obtained by prefixing an existential quantifier to `θ` with respect to the given functions is equivalent to the existence of an element `a` such that the realization of `θ` with respect to the given functions and an `l+1`-tuple obtained by appending `a` to the `l`-tuple defined by the last given function holds. In other words, adding an existential quantifier to a bounded formula `θ` corresponds to the existence of an additional parameter in the realizing environment that satisfies `θ`.
More concisely: For any first order language L, structure M for L, type α, natural number l, bounded formula θ(x₁, ..., xₖ) in L with parameters α and l+1, functions f : α -> M and g : Nat -> M (l), the existence of an element a such that ∃x.(θ(a, x₁, ..., xₖ) ∧ g(l) = f(a)) is equivalent to the realization of ∃x.(θ(x, x₁, ..., xₖ) & ∧ₙi=0.l.(g(i) = f(xₖ₋i))) by f and g.
|
Mathlib.ModelTheory.Order._auxLemma.5
theorem Mathlib.ModelTheory.Order._auxLemma.5 :
∀ {α : Sort u_1} {p q : α → Prop} {a' : α}, (∀ (a : α), a = a' ∨ q a → p a) = (p a' ∧ ∀ (a : α), q a → p a) := by
sorry
The theorem states that for any type `α`, two predicate functions `p` and `q` defined on `α`, and an element `a'` of type `α`, the statement "for all elements `a` of type `α`, `a` being equal to `a'` or `q(a)` implies `p(a)`" is equivalent to the statement "`p(a')` is true and for all elements `a` of type `α`, `q(a)` implies `p(a)`". This theorem essentially relates a certain condition on all elements of a type with a condition on a specific element and all elements satisfying another condition.
More concisely: For any type `α`, predicates `p` and `q` on `α`, and element `a'` of type `α`, the statements "for all `a`, `a = a' ∨ q(a) → p(a)`" and "`p(a')` ∧ (∀a, q(a) → p(a))" are logically equivalent.
|
Mathlib.ModelTheory.Order._auxLemma.15
theorem Mathlib.ModelTheory.Order._auxLemma.15 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ}
{θ : L.BoundedFormula α l.succ} {v : α → M} {xs : Fin l → M},
θ.all.Realize v xs = ∀ (a : M), θ.Realize v (Fin.snoc xs a)
This theorem, `Mathlib.ModelTheory.Order._auxLemma.15`, states that for any first-order language `L`, a type `M` under the structure of `L`, another type `α`, a natural number `l`, a bounded formula `θ` in `L` with `α` and `l+1` as parameters, a function `v` mapping `α` to `M`, and a function `xs` mapping `Fin l` to `M`, the realization of the universal quantification of `θ` with respect to `v` and `xs` is equivalent to the statement that for all `a` in `M`, `θ` is realized with respect to `v` and the `l`-tuple `xs` extended by `a`. In other words, a universal statement in our language is true if and only if the statement is true for every element of `M` when it is added to the end of our `l`-tuple.
More concisely: For any first-order language L, type M, formula θ, functions v from α to M and xs from Fin l to M, the realization of the universal quantification of θ with respect to v and xs is equivalent to θ being true for all a in M when appended to the tuple xs.
|
Mathlib.ModelTheory.Order._auxLemma.12
theorem Mathlib.ModelTheory.Order._auxLemma.12 :
∀ {L : FirstOrder.Language} {α : Type w} {M : Type w'} {n : ℕ} [inst : L.IsOrdered] [inst_1 : L.Structure M]
[inst_2 : LE M] [inst_3 : L.OrderedStructure M] {t₁ t₂ : L.Term (α ⊕ Fin n)} {v : α → M} {xs : Fin n → M},
(t₁.le t₂).Realize v xs =
(FirstOrder.Language.Term.realize (Sum.elim v xs) t₁ ≤ FirstOrder.Language.Term.realize (Sum.elim v xs) t₂)
The theorem `Mathlib.ModelTheory.Order._auxLemma.12` in Lean 4 states that for any first-order language `L` that is ordered, with a structure `M` that is also ordered, and for any terms `t₁` and `t₂` of this language, we can realize a formula that asserts `t₁ ≤ t₂` based on variables `α` (interpreted by `v : α → M`) and `xs : Fin n → M`. This realization is equivalent to saying that the realization of the term `t₁` with the same variable interpretation is less than or equal to the realization of the term `t₂` with the same variable interpretation. In other words, this theorem certifies that the semantic interpretation of the symbolic `≤` in terms of the structure `M` is consistent with the interpretation of the `≤` symbol in the language `L`.
More concisely: For any ordered first-order language `L` and ordered structure `M`, the realization of a formula `t₁ ≤ t₂` in `M` is equivalent to the relationship between the realizations of terms `t₁` and `t₂` in `M`.
|
Mathlib.ModelTheory.Order._auxLemma.6
theorem Mathlib.ModelTheory.Order._auxLemma.6 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {r : L.Relations 2},
M ⊨ r.reflexive = Reflexive fun x y => FirstOrder.Language.Structure.RelMap r ![x, y]
This theorem states that, for any first-order language `L` and any type `M` with a structure for `L`, and for any 2-ary relation symbol `r` in `L`, the sentence that describes `r` as being reflexive in `L` is true in the structure of `M` if and only if `r`, when interpreted as a relation on `M`, is reflexive. Here, a relation is reflexive if it relates every element to itself, i.e., for all `x` in `M`, `r` relates `x` to `x`.
More concisely: For any first-order language L, type M with an L-structure, and 2-ary relation symbol r in L, the relation r is reflexive on M if and only if the formula "∀x, r x x" is true in M.
|
Mathlib.ModelTheory.Order._auxLemma.8
theorem Mathlib.ModelTheory.Order._auxLemma.8 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {r : L.Relations 2},
M ⊨ r.transitive = Transitive fun x y => FirstOrder.Language.Structure.RelMap r ![x, y]
This theorem states that for any first-order language `L` and any type `M` that has a `FirstOrder.Language.Structure` instance, and for any 2-place relation `r` in `L`, the proposition that `r` is transitive in the model `M` (denoted by `M ⊨ FirstOrder.Language.Relations.transitive r`) is equivalent to the relation `r` being transitive in the sense defined by the `Transitive` definition, when `r` is interpreted as a binary relation on `M` via the `FirstOrder.Language.Structure.RelMap` function. In other words, the model theory notion of transitivity for `r` in `M` coincides with the general notion of transitivity for the interpretation of `r` in `M`.
More concisely: For any first-order language L, type M with a Structure instance, and 2-place relation r in L, the model theory condition M ⊨ FirstOrder.Language.Relations.transitive r is equivalent to the relation r being transitive on M as defined by the Transitive relation.
|
Mathlib.ModelTheory.Order._auxLemma.2
theorem Mathlib.ModelTheory.Order._auxLemma.2 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (T : L.Theory), M ⊨ T = ∀ φ ∈ T, M ⊨ φ
This theorem states that for any first-order language `L` and any type `M` that is structured according to `L`, a theory `T` (which is a set of sentences) is true in the model `M` if and only if every sentence `φ` in `T` is true in `M`. Here, `M ⊨ T` denotes that the model `M` satisfies the theory `T`, and `M ⊨ φ` denotes that the model `M` satisfies the sentence `φ`.
More concisely: For any first-order language L and type M structured according to L, a theory T is true in M if and only if every sentence φ in T is true in M (i.e., M ⊨ T if and only if ∀φ ∈ T, M ⊨ φ).
|
Mathlib.ModelTheory.Order._auxLemma.4
theorem Mathlib.ModelTheory.Order._auxLemma.4 : ∀ {α : Type u} {a b : α}, (a ∈ {b}) = (a = b)
This theorem, `Mathlib.ModelTheory.Order._auxLemma.4`, states that for any type `α` and any two elements `a` and `b` of that type, `a` being an element of the set containing only `b` is equivalent to `a` being equal to `b`. In other words, if a set only contains one element, then any item being in this set implies that it must be equal to that single element.
More concisely: For any type `α` and elements `a`, `b` of `α`, if `{a} = {b}` then `a = b`. (Here, `{a}` denotes the singleton set containing `a`.)
|