Rel.ext
theorem Rel.ext : ∀ {α : Type u_1} {β : Type u_2} {r s : Rel α β}, (∀ (a : α), r a = s a) → r = s
The theorem `Rel.ext` states that for any two relations `r` and `s` between two types `α` and `β`, if for every element `a` of type `α`, `r a` is equivalent to `s a`, then the relations `r` and `s` are themselves equivalent. In other words, two relations are considered identical if they agree on the relationship of every individual element from the domain type `α`.
More concisely: If for all `a` in type `α`, `r a ≡ s a`, then `r ≡ s` are equivalent relations.
|
Mathlib.Data.Rel._auxLemma.2
theorem Mathlib.Data.Rel._auxLemma.2 :
∀ {α : Type u_1} {β : Type u_2} (r : Rel α β) (y : β) (s : Set α), (y ∈ r.image s) = ∃ x ∈ s, r x y
The theorem `Mathlib.Data.Rel._auxLemma.2` states that for any two types `α` and `β`, a relation `r` from `α` to `β`, a set `s` of type `α`, and an element `y` of type `β`, the element `y` belongs to the image of the set `s` under the relation `r` if and only if there exists an element `x` belonging to the set `s` such that `r x y` holds. In other words, `y` is in the image of `s` via `r` precisely when there's an element in `s` related to `y` by `r`.
More concisely: For any relation $r$ from type $\alpha$ to type $\beta$, set $s$ of type $\alpha$, and element $y$ of type $\beta$, $y$ lies in the image of $s$ under $r$ if and only if there exists an $x$ in $s$ such that $r(x) = y$.
|
Rel.image_mono
theorem Rel.image_mono : ∀ {α : Type u_1} {β : Type u_2} (r : Rel α β), Monotone r.image
The theorem `Rel.image_mono` states that for all types `α` and `β`, and for any relation `r` from `α` to `β`, the function `Rel.image r` is monotone. In other words, given any types `α` and `β`, and any relation `r` between them, if we have two sets `A` and `B` such that `A` is a subset of `B`, then the image of `A` under the relation `r` is also a subset of the image of `B` under the same relation `r`. This property of the `Rel.image` function is a manifestation of monotonicity where an increase in the input (in terms of set inclusion) leads to an increase in the output (again in terms of set inclusion).
More concisely: For all types `α` and `β` and relations `r` from `α` to `β`, if `A` is a subset of `B`, then `Rel.image r A` is a subset of `Rel.image r B`.
|
Mathlib.Data.Rel._auxLemma.9
theorem Mathlib.Data.Rel._auxLemma.9 :
∀ {α : Sort u_1} {p : α → Prop} {q : (∃ x, p x) → Prop}, (∀ (h : ∃ x, p x), q h) = ∀ (x : α) (h : p x), q ⋯ := by
sorry
The theorem `Mathlib.Data.Rel._auxLemma.9` states that for any type `α`, any predicate `p` on `α`, and any predicate `q` on the existence proof of `p`, the statement "for all existence proofs of `p`, `q` holds" is equivalent to "for all `x` of type `α` for which `p` holds, `q` holds". Here, 'holds' means that the predicate returns true. Essentially, it's stating that the two formulations are equivalent ways of expressing that `q` is true for all `x` for which `p` is true.
More concisely: For any type `α`, predicate `p` on `α`, and predicate `q` on existence proofs of `p`, the statement "for all `x` in `α` with `p(x)`, `q(existence proof of `p`(x))` holds" is equivalent to "for all existence proofs of `p` in `α`, `q` holds".
|
Rel.preimage_mono
theorem Rel.preimage_mono :
∀ {α : Type u_1} {β : Type u_2} (r : Rel α β) {s t : Set β}, s ⊆ t → r.preimage s ⊆ r.preimage t
This theorem, "Rel.preimage_mono", states that for any relation 'r' between two types 'α' and 'β', and any two sets 's' and 't' of type 'β', if set 's' is a subset of set 't', then the preimage of 's' under relation 'r' is a subset of the preimage of 't' under 'r'. In other words, if we have a relation that maps elements from 'α' to 'β', and we have two sets in 'β' such that one is a subset of the other, the set of elements in 'α' that map to the smaller set is a subset of the elements that map to the larger set.
More concisely: If relation r : α → β makes s ⊆ t, then r⁻¹(s) ⊆ r⁻¹(t).
|
Rel.core_inter
theorem Rel.core_inter :
∀ {α : Type u_1} {β : Type u_2} (r : Rel α β) (s t : Set β), r.core (s ∩ t) = r.core s ∩ r.core t
This theorem states that for any relation `r` between two types `α` and `β`, and any two sets `s` and `t` of type `β`, the core of the relation `r` with respect to the intersection of sets `s` and `t` is equal to the intersection of the cores of `r` with respect to sets `s` and `t` individually. In other words, if we consider the elements of `α` that are related through `r` *only* to elements in both `s` and `t`, they form the same set as the intersection of the elements related *only* to elements in `s` and the elements related *only* to elements in `t`.
More concisely: Given a relation `r` between types `α` and `β`, for sets `s` and `t` of type `β`, the core of `r` on `s ∩ t` equals the intersection of the cores of `r` on `s` and `r` on `t`.
|
Rel.core_mono
theorem Rel.core_mono : ∀ {α : Type u_1} {β : Type u_2} (r : Rel α β), Monotone r.core
The theorem `Rel.core_mono` asserts that for any relation `r` from a type `α` to a type `β`, the function `Rel.core r` is monotone. In other words, if we have two sets `s` and `t` of type `β` such that `s` is a subset of `t`, then the core of `s` with respect to the relation `r` is a subset of the core of `t` with respect to the same relation. Here, the "core" of a set `s` with respect to a relation `r` is defined as the set of elements in `α` that only relate to elements in `s` through `r`.
More concisely: For any relation `r` from type `α` to type `β`, the function `Rel.core r` maps subset inclusion of `β` to subset inclusion of `α` in the sense that if `s` is a subset of `t`, then the core of `s` with respect to `r` is a subset of the core of `t` with respect to `r`.
|