Subtype.map.proof_1
theorem Subtype.map.proof_1 :
∀ {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β),
(∀ (a : α), p a → q (f a)) → ∀ (x : Subtype p), q (f ↑x)
This theorem states that for any two types `α` and `β`, predicates `p` on `α` and `q` on `β`, and a function `f` from `α` to `β`, if for all elements `a` of type `α` the property `p a` implies the property `q` on `f a`, then for all subtypes `x` of type `α` satisfying the property `p`, the property `q` holds on `f` applied to `x`. In other words, the theorem ensures that if `f` maps elements of `α` satisfying `p` to elements of `β` satisfying `q`, then `f` also maps elements of the subtype of `α` defined by `p` to elements of `β` satisfying `q`.
More concisely: If `f: α → β`, `p` is a predicate on `α`, `q` is a predicate on `β`, and for all `a: α` with `p a`, `q (f a)` holds, then `q` holds for `f` applied to every subtype `x` of `α` satisfying `p`.
|
Subtype.prop
theorem Subtype.prop : ∀ {α : Sort u_1} {p : α → Prop} (x : Subtype p), p ↑x
This theorem, `Subtype.prop`, states that for any type `α` and any property `p` that `α` might satisfy, if you have a subtype `x` of `α` that satisfies property `p`, then the property `p` holds for the coercion of `x` (i.e., `x` considered as an object of the original type `α`). This is similar to the `Subtype.mem` result in `Data.Set.Basic`. Essentially, it guarantees that any member of a subtype still satisfies the defining property of that subtype when viewed as a member of the original type.
More concisely: If `x` is a subtype element of type `α` satisfying property `p`, then `p` holds for the coercion of `x` in type `α`.
|
Subtype.ne_of_val_ne
theorem Subtype.ne_of_val_ne : ∀ {α : Sort u_1} {p : α → Prop} {a b : Subtype p}, ↑a ≠ ↑b → a ≠ b
This theorem, named 'Subtype.ne_of_val_ne', states that for any type 'α' and any predicate 'p' on 'α', if we have two elements 'a1' and 'a2' of the subtype of 'α' satisfying 'p', then if their underlying values in 'α' are not equal (i.e., `↑a1 ≠ ↑a2`), the original elements 'a1' and 'a2' are also not equal. In other words, distinct elements in the original type lead to distinct elements in the subtype.
More concisely: For any type α and predicate p, if a1 and a2 are distinct elements in the subtype {x : α | p x}, then ↑a1 and ↑a2 are distinct in α.
|
Subtype.ext_iff_val
theorem Subtype.ext_iff_val : ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
This theorem, `Subtype.ext_iff_val`, states that for any type `α` and a predicate `p` that applies to `α`, two elements `a1` and `a2` of the subtype `{ x // p x }` (i.e., the subset of `α` for which `p` holds) are equal if and only if their underlying values (`↑a1` and `↑a2`) in `α` are equal. In other words, two elements of a subtype are equal if and only if their corresponding elements in the original type are equal.
More concisely: For any type $\alpha$ and predicate $p$, elements $a\_1$ and $a\_2$ of the subtype ${x // p(x)}$ are equal if and only if their underlying values in $\alpha$ are equal.
|
Subtype.val_injective
theorem Subtype.val_injective : ∀ {α : Sort u_1} {p : α → Prop}, Function.Injective Subtype.val
The theorem `Subtype.val_injective` states that for any type `α` and a property `p` defined for `α`, the function `Subtype.val` is injective. In other words, if we have two subtypes `s1` and `s2` of `α` that satisfy the property `p`, and if `Subtype.val s1` is equal to `Subtype.val s2`, then `s1` and `s2` are the same. This essentially says that the `Subtype.val` function does not map different subtypes to the same value in `α`.
More concisely: If `s1` and `s2` are subtypes of a type `α` such that `p(x)` holds for all `x ∈ s1` and `x ∈ s2`, then `Subtype.val s1 = Subtype.val s2` implies `s1 = s2`.
|
Subtype.coe_prop
theorem Subtype.coe_prop : ∀ {α : Type u_1} {S : Set α} (a : { a // a ∈ S }), ↑a ∈ S
This theorem, `Subtype.coe_prop`, states that for any given type `α` and any set `S` of that type, if we have a subtype `a` such that `a` belongs to `S`, then the underlying element of `a` (obtained through the coercion function `↑a`) also belongs to the set `S`. In simpler terms, it guarantees that an element of a subtype, which is defined as belonging to a particular set, indeed belongs to that set when we "unwrap" it from the subtype.
More concisely: For any type `α` and set `S` of `α`, if `a` is an element of the subtype `s : Subset α S` then `↑a` belongs to `S`.
|
Mathlib.Data.Subtype._auxLemma.2
theorem Mathlib.Data.Subtype._auxLemma.2 :
∀ {α : Sort u_1} {p : α → Prop} {q : { a // p a } → Prop}, (∃ x, q x) = ∃ a, ∃ (b : p a), q ⟨a, b⟩
This theorem is stating that for any type `α`, and any predicates `p` over `α` and `q` over the subtype `{ a // p a }`, the statement "there exists an element in the subtype such that `q` holds" is equivalent to "there exists an element `a` in the type `α` such that `p` holds for `a`, and `q` holds for the subtype element composed of `a` and the proof `b` that `p a` is true". In other words, it shows the equivalence between existential quantification over subtypes and existential quantification over the original types with corresponding predicates.
More concisely: For any type `α`, predicate `p` over `α`, and predicate `q` over the subtype `{ a // p a },` the existence of an element in the subtype satisfying `q` is equivalent to the existence of an element in `α` satisfying `p` and the corresponding subtype element with proof `p a` satisfying `q`.
|
Subtype.ext_iff
theorem Subtype.ext_iff : ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
This theorem, `Subtype.ext_iff`, states that for any type `α`, any predicate `p` on `α`, and any two elements `a1` and `a2` of the subtype `{x // p x}`, `a1` is equal to `a2` if and only if the underlying elements of `a1` and `a2` (denoted by `↑a1` and `↑a2`) in `α` are equal. In other words, two elements of a subtype are equal if and only if their corresponding elements in the parent type are equal.
More concisely: For any type `α` and predicate `p` on `α`, elements `a1` and `a2` of the subtype `{x // p x}` are equal if and only if the underlying elements `↑a1` and `↑a2` in `α` are equal.
|
Subtype.forall'
theorem Subtype.forall' :
∀ {α : Sort u_1} {p : α → Prop} {q : (x : α) → p x → Prop},
(∀ (x : α) (h : p x), q x h) ↔ ∀ (x : { a // p a }), q ↑x ⋯
This theorem, named `Subtype.forall'`, states an alternative version of `Subtype.forall`. For any type `α` and properties `p` (which is a predicate on `α`) and `q` (which is a predicate on `α` and a proof of `p`), this theorem asserts that the statement "for all `x` of type `α` for which `p` holds, property `q` also holds" is equivalent to the statement "for all `x` in the subtype of `α` defined by `p`, property `q` holds". This version can be useful if Lean cannot infer `q` when using `Subtype.forall` from right to left.
More concisely: For any type `α` and predicates `p` and `q` on `α` with `p` implying `q`, the statements "for all `x` of type `α` with `p(x)`, `q(x)` holds" and "for all `x` in the subtype of `α` defined by `p`, `q(x)` holds" are equivalent.
|
Subtype.exists'
theorem Subtype.exists' :
∀ {α : Sort u_1} {p : α → Prop} {q : (x : α) → p x → Prop}, (∃ x, ∃ (h : p x), q x h) ↔ ∃ x, q ↑x ⋯
This theorem, `Subtype.exists'`, provides an alternative version of `Subtype.exists`. It states that for any type `α` and any properties `p` and `q` where `q` is a property of `x : α` and `h : p x`, the existence of an `x` and `h` such that `q x h` holds is logically equivalent to the existence of an `x` such that `q ↑x` holds. This version of the theorem can be useful in situations where Lean's type inference is unable to determine `q` when using `Subtype.exists` from right to left.
More concisely: For any type α and properties p and q, the existence of an x : α and h : p x such that q x h holds is equivalent to the existence of an x such that q (x :> α) holds.
|
Mathlib.Data.Subtype._auxLemma.5
theorem Mathlib.Data.Subtype._auxLemma.5 : ∀ {α : Type u_1} {S : Set α} (a : { a // a ∈ S }), (↑a ∈ S) = True := by
sorry
The theorem `Mathlib.Data.Subtype._auxLemma.5` states that for any type `α` and any set `S` of type `α`, for every element `a` that is an element of `S` (specifically, `a` is a subtype of `α` such that `a` is in `S`), it is always true that `a` belongs to `S`. This theorem is essentially asserting the fundamental property of element-set membership: if an element is defined as belonging to a set, then it indeed belongs to that set.
More concisely: For any type `α` and set `S` of `α`, any element `a` that is a subtype of `α` and is in `S`, belongs to `S`.
|
Subtype.ext
theorem Subtype.ext : ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
This theorem, `Subtype.ext`, states that for any type `α`, any predicate `p` on `α`, and any two elements `a1` and `a2` of the subtype consisting of those elements `x` of `α` for which `p x` holds, if the elements `a1` and `a2` are equal when considered as elements of the base type `α` (i.e., `↑a1 = ↑a2` where `↑` denotes the coercion from the subtype to the base type), then `a1` and `a2` must also be equal as elements of the subtype. In other words, two elements of a subtype are equal if and only if they are equal in the base type.
More concisely: For any type `α` and subtype `p ⊆ α`, if `a₁` and `a₂` are equal as elements of `α` and belong to `p`, then they are equal as elements of `p`.
|
Subtype.forall
theorem Subtype.forall :
∀ {α : Sort u_1} {p : α → Prop} {q : { a // p a } → Prop},
(∀ (x : { a // p a }), q x) ↔ ∀ (a : α) (b : p a), q ⟨a, b⟩
This theorem, `Subtype.forall`, states a property about subtypes in Lean. In detail, for any type `α`, a predicate `p` on `α`, and a predicate `q` on subtypes `{ a // p a }` (i.e., elements of `α` that satisfy `p`), it asserts that the statement "for all elements `x` of the subtype `{ a // p a }`, `q` is true on `x`" is equivalent to the statement "for all elements `a` of the type `α`, if `a` satisfies `p` (denoted by `b : p a`), then `q` is true on the element `{ val := a, property := b }` of the subtype". Here, `{ val := a, property := b }` is the explicit construction of an element of the subtype `{ a // p a }` from `a : α` and `b : p a`.
More concisely: For any type α, predicate p on α, and subtype { a // p a }, the property "for all x in { a // p a }, q(x) holds" is equivalent to "for all a in α, if p(a) holds then q({ val := a, property := p a }) holds".
|
Subtype.coe_mk
theorem Subtype.coe_mk : ∀ {α : Sort u_1} {p : α → Prop} (a : α) (h : p a), ↑⟨a, h⟩ = a
This theorem states that for all types `α` and any predicate `p` on `α`, given an element `a` of `α` and a proof `h` that `a` satisfies the predicate `p`, the coercion (indicated by `↑`) of a subtype formed with `a` and `h` is equal to `a`. This essentially means that the subtype element `{ val := a, property := h }` behaves like `a` whenever it is used in a context where `α` is expected.
More concisely: For all types `α` and predicates `p` on `α`, the coercion of an element `a` of `α` with proof `h` that `a` satisfies `p` is equal to `a`. In other words, the subtype element `{ val := a, property := h }` behaves like `a`.
|
Mathlib.Data.Subtype._auxLemma.1
theorem Mathlib.Data.Subtype._auxLemma.1 :
∀ {α : Sort u_1} {p : α → Prop} {q : { a // p a } → Prop},
(∀ (x : { a // p a }), q x) = ∀ (a : α) (b : p a), q ⟨a, b⟩
This theorem states that, for any type `α`, any property `p` of `α`, and any property `q` of the subtype of `α` satisfying `p`, the proposition that `q` applies to all elements of the subtype is equivalent to the proposition that, for all elements `a` of `α` and proofs `b` that `a` satisfies `p`, `q` applies to the subtype element composed of `a` and `b`. This is a theorem about the relationship between properties of a subtype and properties of the elements in the underlying type.
More concisely: For any type `α`, property `p` of `α`, and property `q` of its subtype satisfying `p`, the subtype elementwise satisfies `q` if and only if `q` applies to all elements in the subtype with proofs of `p`.
|
Subtype.exists
theorem Subtype.exists :
∀ {α : Sort u_1} {p : α → Prop} {q : { a // p a } → Prop}, (∃ x, q x) ↔ ∃ a, ∃ (b : p a), q ⟨a, b⟩
This theorem, `Subtype.exists`, states that for any type `α`, any property `p` on `α`, and any property `q` on elements `a` of type `α` satisfying `p`, there exists an element `x` such that the property `q` holds for `x` if and only if there exists an element `a` and a proof `b` that `a` satisfies `p`, such that `q` holds for `a` with the proof `b`. This theorem essentially shows the equivalence between finding an element in a subtype (a type with an additional property) satisfying some conditions and finding an element in the original type with a proof that it satisfies the conditions of the subtype and the additional conditions.
More concisely: For any type `α`, property `p` on `α`, and property `q` on elements `a` satisfying `p`, there exists an element `x` of type `α` with property `q` if and only if there exists an element `a` of type `α` satisfying `p` and a proof that `a` has property `p`, with `q` holding for `a` under this proof.
|
Subtype.coe_inj
theorem Subtype.coe_inj : ∀ {α : Sort u_1} {p : α → Prop} {a b : Subtype p}, ↑a = ↑b ↔ a = b
This theorem, named `Subtype.coe_inj`, states that for any type `α` and a predicate `p` over `α`, if `a` and `b` are instances of the subtype `p`, then the coercion of `a` to `α` is equal to the coercion of `b` to `α` if and only if `a` is equal to `b`. In other words, distinct elements of the subtype remain distinct when coerced to the base type. This is a statement about the injectivity of the coercion function from the subtype to the base type.
More concisely: If `α` is a type and `p` is a predicate on `α`, then for all `a` and `b` in the subtype `p ⊆ α`, the coercion of `a` to `α` equals the coercion of `b` to `α` if and only if `a` equals `b`.
|
Subtype.ext_val
theorem Subtype.ext_val : ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
This theorem, `Subtype.ext_val`, states that for any type `α` and any predicate `p` over `α`, if you have two elements `a1` and `a2` of the subtype `{x // p x}` (that is, the set of elements of `α` for which `p` holds true), if the underlying elements of `a1` and `a2` (obtained by the coercion function `↑`) are equal, then `a1` and `a2` are also equal. Essentially, it's saying that two elements of a subtype are equal if and only if the elements they represent in the parent type are equal.
More concisely: For any type `α` and predicate `p` over `α`, elements `a1` and `a2` of the subtype `{x // p x}` are equal if and only if their underlying elements `↑a1` and `↑a2` are equal.
|
Subtype.coe_injective
theorem Subtype.coe_injective : ∀ {α : Sort u_1} {p : α → Prop}, Function.Injective fun a => ↑a
The theorem `Subtype.coe_injective` states that for any type `α` and any predicate `p` on `α`, the function that maps an element `a` of the subtype `{a : α | p a}` to its corresponding element in `α` (denoted `↑a` or `coe a`) is injective. In other words, no two distinct elements of the subtype map to the same element in `α` under the coercion function. In mathematical terms, if `a` and `b` are elements of the subtype and `↑a = ↑b`, then `a = b`.
More concisely: If `a` and `b` are elements of the subtype `{a : α | p a}`, then `↑a = ↑b` implies `a = b`.
|
Subtype.mk_eq_mk
theorem Subtype.mk_eq_mk :
∀ {α : Sort u_1} {p : α → Prop} {a : α} {h : p a} {a' : α} {h' : p a'}, ⟨a, h⟩ = ⟨a', h'⟩ ↔ a = a'
This theorem states that for every type `α`, and a predicate `p` on `α`, for any two elements `a` and `a'` of type `α` satisfying the predicate `p` (denoted by `h` and `h'`), the subtypes created by these elements and their respective properties are equal if and only if the elements `a` and `a'` are equal. Essentially, two subtypes are equal when their underlying elements in the original type are equal.
More concisely: For all types `α` and predicates `p` on `α`, if `a` and `a'` are elements of type `α` satisfying `p`, then the subtypes `{x : α | p x} at a` and `{x : α | p x} at a'` are equal if and only if `a` is equal to `a'`.
|
Subtype.coind_injective
theorem Subtype.coind_injective :
∀ {α : Sort u_4} {β : Sort u_5} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)),
Function.Injective f → Function.Injective (Subtype.coind f h)
The theorem `Subtype.coind_injective` states that for any types `α` and `β`, any function `f : α → β`, and any property `p` of type `β → Prop` such that `p` holds for all `f(a)` where `a` is of type `α`, if the function `f` is injective (meaning that whenever `f(x) = f(y)`, it implies `x = y`), then the function `Subtype.coind f h` is also injective. Here, `Subtype.coind f h` is a function that maps each element of type `α` to a subtype (a subset of a given type) of type `β` satisfying the property `p`, constructed by applying `f` to the element of type `α`.
More concisely: If `f : α → β` is an injective function and `p (β) : Prop` holds for all `f(a)` in `α`, then `Subtype.coind f h` is an injective function from `α` to the collection of subtypes of `β` satisfying `p`.
|
Subtype.coe_eta
theorem Subtype.coe_eta : ∀ {α : Sort u_1} {p : α → Prop} (a : { a // p a }) (h : p ↑a), ⟨↑a, h⟩ = a
This theorem, `Subtype.coe_eta`, states that for any type `α` and any property `p` defined on elements of `α`, for each element `a` of the subtype `{ a // p a }` (i.e., the set of elements `a` in `α` for which `p(a)` holds) and whenever `p` holds for the coercion of `a` (notated `↑a`), the object created by the subtype constructor `{ val := ↑a, property := h }` is the same as `a` itself. Basically, it proves that if `a` is an element of a subtype characterized by a property `p`, then the element `a` can be reconstructed from its coerced value `↑a` and its property `h`.
More concisely: For any type `α` and property `p` on `α`, if `a` is an element of the subtype `{ x // p x }` and `p (↑a)` holds, then `a = { val := ↑a, property := rfl }`.
|