IsAntichain.eq'
theorem IsAntichain.eq' :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsAntichain r s → ∀ {a b : α}, a ∈ s → b ∈ s → r b a → a = b := by
sorry
The theorem `IsAntichain.eq'` states that for any type `α`, relation `r`, and set `s` of elements of type `α`, if `s` is an antichain with respect to the relation `r`, then for any elements `a` and `b` in `s`, if `r b a` holds, then `a` must be equal to `b`. In other words, in an antichain, no two distinct elements are related in the reverse order.
More concisely: In an antichain, if element `a` is related to element `b` (`r b a`), then `a` equals `b`.
|
IsAntichain.image_relEmbedding_iff
theorem IsAntichain.image_relEmbedding_iff :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} {φ : r ↪r r'},
IsAntichain r' (⇑φ '' s) ↔ IsAntichain r s
This theorem states that for any two types `α` and `β`, and two relations `r` on `α` and `r'` on `β`, along with a set `s` of type `α` and a relation-embedding `φ` from `r` to `r'`, the image of the set `s` under the map `φ` is an antichain with respect to `r'` if and only if the set `s` is an antichain with respect to `r`. In simpler terms, it means that mapping an antichain through a relation-embedding preserves the property of being an antichain.
More concisely: For any relations `r` on type `α` and `r'` on type `β`, set `s` of type `α`, and relation-embedding `φ` from `r` to `r'`, if `s` is an antichain with respect to `r`, then the image of `s` under `φ` is an antichain with respect to `r'`.
|
IsAntichain.eq
theorem IsAntichain.eq :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsAntichain r s → ∀ {a b : α}, a ∈ s → b ∈ s → r a b → a = b := by
sorry
The theorem `IsAntichain.eq` states that for any type `α` and any relation `r` on `α`, if a set `s` of type `α` is an antichain with respect to `r` (meaning that no two distinct elements in `s` are related by `r`), then for any two elements `a` and `b` in `s`, if `a` is related to `b` by `r`, then `a` must be equal to `b`. In other words, this theorem asserts that in an antichain, no two distinct elements can be related, which is consistent with the definition of an antichain.
More concisely: In an antichain, distinct elements are not related by the given relation.
|
IsAntichain.flip
theorem IsAntichain.flip : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsAntichain r s → IsAntichain (flip r) s
The theorem `IsAntichain.flip` states that for any type `α`, any binary relation `r` on `α`, and any set `s` of `α`, if `s` is an antichain with respect to `r`, it is also an antichain with respect to the flipped relation of `r`. In other words, if no two distinct elements in `s` are related by `r`, then no two distinct elements are related by the flipped (reverse) `r` either. This theorem is about the invariance of the property of being an antichain under the operation of flipping the order of arguments in the relation.
More concisely: If `s` is an antichain of a binary relation `r` on type `α`, then `s` is also an antichain of the flipped relation of `r`.
|
IsAntichain.image_relEmbedding
theorem IsAntichain.image_relEmbedding :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α},
IsAntichain r s → ∀ (φ : r ↪r r'), IsAntichain r' (⇑φ '' s)
The theorem `IsAntichain.image_relEmbedding` states that for all types `α` and `β`, and for all relations `r` on `α` and `r'` on `β`, if `s` is an antichain with respect to `r`, then the image of `s` under any relation embedding `φ` from `r` to `r'` is an antichain with respect to `r'`. Informally, this means that if we have a set where no two distinct elements are related by a specific relation, then if we map this set to a new set using a function that preserves the relation, the new set also has the property that no two distinct elements are related.
More concisely: If `s` is an antichain for relation `r` on type `α`, and `φ` is a relation embedding from `r` to `r'` on type `β`, then the image of `s` under `φ` is an antichain for relation `r'` on `β`.
|
IsAntichain.to_dual
theorem IsAntichain.to_dual :
∀ {α : Type u_1} {s : Set α} [inst : LE α],
IsAntichain (fun x x_1 => x ≤ x_1) s → IsAntichain (fun x x_1 => x ≤ x_1) s
The theorem `IsAntichain.to_dual` states that for any type `α` and any set `s` of elements of this type, where the elements of `α` have a less than or equal to (`≤`) relation, if `s` is an antichain with respect to the `≤` relation, then `s` is also an antichain with respect to the dual of the `≤` relation. In other words, if no two distinct elements in `s` are related by `≤`, then no two distinct elements in `s` are related by the opposite relation as well.
More concisely: If `s` is an antichain of a partially ordered type `α` with respect to the relation `≤`, then `s` is also an antichain with respect to the dual relation `>=`.
|
IsAntichain.preimage_relEmbedding
theorem IsAntichain.preimage_relEmbedding :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {t : Set β},
IsAntichain r' t → ∀ (φ : r ↪r r'), IsAntichain r (⇑φ ⁻¹' t)
The theorem `IsAntichain.preimage_relEmbedding` states that for any types `α` and `β`, any relations `r` on `α` and `r'` on `β`, and any set `t` of type `β`, if `t` forms an antichain with respect to the relation `r'`, then for any relation embedding `φ` from `r` to `r'`, the preimage of `t` under `φ` forms an antichain with respect to the relation `r` on `α`. In other words, the preimage of an antichain under a relation-preserving function is also an antichain.
More concisely: If `t` is an antichain of relation `r'` on type `β` and `φ` is a relation embedding from relation `r` on type `α` to `r'`, then the preimage of `t` under `φ` is an antichain of relation `r` on `α`.
|