• API
• FAQ
• Tools
• Archive
SHARE
TWEET

# Untitled

a guest Nov 21st, 2019 80 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. Theorem “Weakening for ∩”: Q ∩ R ⊆ Q  ∧  Q ∩ R ⊆ R
2. Proof:
3.     By “Characterisation of ∩”, “Reflexivity of ⊆”
4.
5. Theorem “Symmetry of ∩”: Q ∩ R  ⊆  R ∩ Q
6. Proof:
7.     By “Characterisation of ∩”, “Reflexivity of ⊆”
8.
9. Corollary “Symmetry of ∩”: Q ∩ R  =  R ∩ Q
10. Proof:
11.     Q ∩ R  =  R ∩ Q
12.   =⟨ “Mutual inclusion” ⟩
13.     Q ∩ R ⊆ R ∩ Q ∧ R ∩ Q ⊆ Q ∩ R
14.   =⟨ “Symmetry of ∩”, “Identity of ∧” ⟩
15.     R ∩ Q ⊆ Q ∩ R
16.   =⟨ “Characterisation of ∩” ⟩
17.     R ∩ Q ⊆ Q ∧  R ∩ Q ⊆ R
18.   =⟨ “Characterisation of ∩” ⟩
19.     R ∩ Q ⊆ R ∩ Q
20.   =⟨ “Reflexivity of ⊆” ⟩
21.     true
22.
23. Theorem “Associativity of ∩”: (Q ∩ R) ∩ S  ⊆  Q ∩ (R ∩ S)
24. Proof:
25.    By “Characterisation of ∩”, “Reflexivity of ⊆”
26.
27. Corollary “Associativity of ∩”: (Q ∩ R) ∩ S  =  Q ∩ (R ∩ S)
28. Proof:
29.     (Q ∩ R) ∩ S  =  Q ∩ (R ∩ S)
30.   =⟨ “Mutual inclusion” ⟩
31.     (Q ∩ R) ∩ S ⊆ Q ∩ (R ∩ S) ∧ Q ∩ (R ∩ S) ⊆ (Q ∩ R) ∩ S
32.   =⟨ “Associativity of ∩”, “Identity of ∧” ⟩
33.     Q ∩ (R ∩ S) ⊆ (Q ∩ R) ∩ S
34.   =⟨ “Characterisation of ∩” ⟩
35.     Q ∩ (R ∩ S) ⊆ Q ∩ (R ∩ S)
36.   =⟨ “Reflexivity of ⊆” ⟩
37.     true
38.
39. Theorem “Idempotency of ∩”: R ∩ R = R
40. Proof:
41.     R ∩ R = R
42.   =⟨ “Mutual inclusion” ⟩
43.     R ∩ R ⊆ R ∧ R ⊆ R ∩ R
44.   =⟨ “Characterisation of ∩” ⟩
45.     R ∩ R ⊆ R ∧ R ⊆ R ∧ R ⊆ R
46.   =⟨ “Reflexivity of ⊆”, “Identity of ∧” ⟩
47.     R ∩ R ⊆ R
48.   =⟨ “Characterisation of ∩” ⟩
49.     R ∩ R ⊆ R
50.   =⟨ “Idempotency of ∧” ⟩
51.     R ∩ R ⊆ R ∧ R ∩ R ⊆ R — This is “Weakening for ∩”
52.
53. Theorem “Monotonicity of ∩”: Q ⊆ R  ⇒  Q ∩ S ⊆ R ∩ S
54. Proof:
55.     Q ⊆ R ⇒ Q ∩ S ⊆ R ∩ S
56.   ≡⟨ “Characterisation of ∩” ⟩
57.     Q ⊆ R ⇒ (Q ∩ S ⊆ R) ∧ (S ∩ Q ⊆ S)
58.   ≡⟨ “Idempotency of ∧” and “Weakening for ∩” ⟩
59.     Q ⊆ R ⇒ (Q ∩ S ⊆ R) ∧ true
60.   ≡⟨ “Identity of ∧” ⟩
61.     Q ⊆ R ⇒ (Q ∩ S ⊆ R)
62.   ⇐⟨ “Transitivity of ⊆” ⟩
63.     Q ∩ S ⊆ Q
64.   ≡⟨ “Idempotency of ∧” and “Weakening for ∩” ⟩
65.     true
66.
67. Theorem “Inclusion via ∩”: Q ⊆ R  ≡  Q ∩ R = Q
68. Proof:
69.   Using “Mutual implication”:
70.     Subproof for `Q ⊆ R  ⇒  Q ∩ R = Q`:
71.       Assuming `Q ⊆ R`:
72.           Q ∩ R = Q
73.         =⟨ “Mutual inclusion” ⟩
74.           Q ∩ R ⊆ Q ∧ Q ⊆ Q ∩ R
75.         =⟨ “Characterisation of ∩” ⟩
76.           Q ∩ R ⊆ Q ∧ Q ⊆ Q ∧ Q ⊆ R
77.         =⟨ “Reflexivity of ⊆”, Assumption `Q ⊆ R`, “Identity of ∧” ⟩
78.           Q ∩ R ⊆ Q
79.         =⟨ “Idempotency of ∧”, “Weakening for ∩” ⟩
80.           true
81.     Subproof for `Q ∩ R = Q ⇒ Q ⊆ R`:
82.       Assuming `Q ∩ R = Q`:
83.           Q ⊆ R
84.         =⟨ Assumption `Q ∩ R = Q` ⟩
85.           Q ∩ R ⊆ R
86.         =⟨ “Idempotency of ∧”, “Weakening for ∩” ⟩
87.           true
88.
89. Theorem “Converse of ∩”:     (R ∩ S) ˘  ⊆  R ˘ ∩ S ˘
90. Proof:
91.     (R ∩ S) ˘ ⊆  R ˘ ∩ S ˘
92.   ≡⟨ “Characterisation of ∩” ⟩
93.     (R ∩ S) ˘ ⊆  R ˘ ∧ (R ∩ S) ˘ ⊆ S ˘
94.   =⟨ “Isotonicity of ˘” ⟩
95.     (R ∩ S) ⊆  R ∧ (R ∩ S) ⊆ S
96.   =⟨ “Characterisation of ∩” ⟩
97.     (R ∩ S) ⊆  R ∩ S
98.   =⟨ “Reflexivity of ⊆” ⟩
99.     true
100.
101. Theorem “Converse of ∩”:     (R ∩ S) ˘  =  R ˘ ∩ S ˘
102. Proof:
103.     (R ∩ S) ˘  =  R ˘ ∩ S ˘
104.   =⟨ “Mutual inclusion” ⟩
105.     (R ∩ S) ˘ ⊆ R ˘ ∩ S ˘ ∧ R ˘ ∩ S ˘ ⊆ (R ∩ S) ˘
106.   =⟨ “Converse of ∩”, “Identity of ∧” ⟩
107.     R ˘ ∩ S ˘ ⊆ (R ∩ S) ˘
108.   =⟨ “Self-inverse of ˘”, “Isotonicity of ˘” ⟩
109.     (R ˘ ∩ S ˘) ˘ ⊆ (R ∩ S)
110.   =⟨ “Characterisation of ∩” ⟩
111.     (R ˘ ∩ S ˘) ˘ ⊆ R ∧ (R ˘ ∩ S ˘) ˘ ⊆ S
112.   =⟨ “Self-inverse of ˘”, “Isotonicity of ˘” ⟩
113.     R ˘ ∩ S ˘ ⊆ R ˘ ∧ R ˘ ∩ S ˘ ⊆ S ˘
114.   =⟨ “Weakening for ∩”, “Idempotency of ∧” ⟩
115.     true
116.
117. Theorem “Sub-distributivity of ⨾ over ∩”:
118.     Q ⨾ (R ∩ S)  ⊆  Q ⨾ R  ∩  Q ⨾ S
119. Proof:
120.     Q ⨾ (R ∩ S)
121.   =⟨ “Idempotency of ∩” ⟩
122.     Q ⨾ (R ∩ S) ∩ Q ⨾ (R ∩ S)
123.   ⊆⟨ “Monotonicity of ∩” with “Monotonicity of ⨾” with “Weakening for ∩” ⟩
124.     Q ⨾ (R ∩ S) ∩ Q ⨾ S
125.   ⊆⟨ “Monotonicity of ∩” with “Monotonicity of ⨾” with “Weakening for ∩” ⟩
126.     Q ⨾ (R) ∩ Q ⨾ S
127.
128. Theorem “Antisymmetry of converse”:  is-antisymmetric R  ≡  is-antisymmetric (R ˘)
129. Proof:
130.     is-antisymmetric R
131.   =⟨ “Definition of antisymmetry” ⟩
132.     R ∩ R ˘ ⊆ Id
133.   =⟨ “Self-inverse of ˘” ⟩
134.     R ˘ ∩ R ˘ ˘ ⊆ Id
135.   =⟨ “Definition of antisymmetry” ⟩
136.     is-antisymmetric (R ˘)
137.
138. Theorem “Converse of an order”:  is-order E  ≡  is-order (E ˘)
139. Proof:
140.     is-order E
141.   =⟨ “Definition of ordering” ⟩
142.     is-reflexive E ∧ is-antisymmetric E ∧ is-transitive E
143.   =⟨ “Reflexivity of converse”, “Antisymmetry of converse”, “Transitivity of converse” ⟩
144.     is-reflexive (E ˘) ∧ is-antisymmetric (E ˘) ∧ is-transitive (E ˘)
145.   =⟨ “Definition of ordering” ⟩
146.     is-order (E ˘)
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.

Top