Set.mem_op
theorem Set.mem_op : ∀ {α : Type u_1} {s : Set α} {a : αᵒᵖ}, a ∈ s.op ↔ a.unop ∈ s
This theorem states that for any type `α`, any set `s` of type `α`, and any element `a` of the opposite type of `α`, `a` is a member of the opposite set of `s` (that is, the set obtained by taking the opposite of each member of `s`) if and only if the "unop-ed" version of `a` (that is, `a` with the operation of taking the opposite reversed) is a member of `s`. In other words, we can check set membership for an entity in an opposite set by "reversing" the entity back to its original form and checking its membership in the original set.
More concisely: For any type `α`, set `s` of `α`, and its opposite element `a`, `a` is in the opposite set of `s` if and only if the opposition of `a` is in `s`.
|
Set.unop_op
theorem Set.unop_op : ∀ {α : Type u_1} (s : Set αᵒᵖ), s.unop.op = s
The theorem `Set.unop_op` states that for any type `α` and for any set `s` of elements of type `α`'s opposite, the operation of first applying the `unop` operation on `s` (which converts each of its elements to the opposite type) and then applying the `op` operation (converting them back to the original type) leaves the set `s` unchanged. This theorem captures the idea that these two operations are inverses of each other in the context of sets.
More concisely: For any set `s` of type `α`, the application of `op` after `unop` on the elements of `s` results in the original set `s`. In other words, `unop` and `op` are inverse operations on sets of type `α`.
|
Set.singleton_op
theorem Set.singleton_op : ∀ {α : Type u_1} (x : α), {x}.op = {Opposite.op x}
The theorem `Set.singleton_op` states that for any type `α` and any element `x` of type `α`, the opposite of the singleton set containing `x` is the singleton set containing the opposite of `x`. Here, "opposite" refers to the operation defined by `Set.op` and `Opposite.op`, which involve reversing or "flipping" the elements of a set and the elements of a type, respectively.
More concisely: For any type `α` and element `x` of `α`, the opposite of the singleton set `{x}` is the singleton set `{op x}`, where `op` is the opposite operation.
|
Set.singleton_unop
theorem Set.singleton_unop : ∀ {α : Type u_1} (x : αᵒᵖ), {x}.unop = {x.unop}
The theorem `Set.singleton_unop` states that for every type `α` and for any term `x` of the opposite type `αᵒᵖ`, the unary operation (unop) of a singleton set containing `x` is equal to the singleton set containing the unary operation of `x`. This essentially means that applying the unary operation to each member of a singleton set is the same as applying the unary operation to the singleton set itself.
More concisely: For any type `α` and term `x` of opposite type `αᵒᵖ`, the unary operation of the singleton set `{x}´ is equal to the singleton set `{unop x}`.
|
Set.op_mem_op
theorem Set.op_mem_op : ∀ {α : Type u_1} {s : Set α} {a : α}, Opposite.op a ∈ s.op ↔ a ∈ s
This theorem states that for any type `α`, any set `s` of type `α`, and any element `a` of type `α`, the element 'a' is a member of the set 's' if and only if the opposite of 'a' is a member of the opposite set of 's'. Here, the 'opposite' of an element or a set is defined using the `Opposite.op` and `Set.op` functions, respectively.
More concisely: For any type `α`, set `s` of type `α`, and element `a` of type `α`, `a` is in `s` if and only if the opposite of `a` is in the opposite of `s`.
|