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. OK, I Understand
 
Top