Commits

ppavel committed 53bee43 Draft

Пример работы с тем, что я планирую доказать в будущем

Comments (0)

Files changed (2)

   field
     +-monotonicity : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
     0≤1 : 0≤ 1#
+    -- это легко доказывается. см. замечания в Probability
+    a≈b→c+a≈c+b : ∀ {a b} →  a ≈ b → ∀ c → c + a ≈ c + b
+
   totalOrder : TotalOrder zero zero zero
   totalOrder = record { Carrier = Num; _≈_ = _≈_; _≤_ = _≤_; isTotalOrder = isTotalOrder }
 
   open POR {{...}}
   open import Data.Product using (proj₁ ; proj₂)
 
+
   0≤b→a+b≈c→a≤c : ∀ {a b c}  →  0# ≤ b → a + b ≈ c  → a ≤ c
   0≤b→a+b≈c→a≤c  {a} {b} {c} 0≤b a+b≈c  = 
     begin
           -- лень разбираться с областями видимости и в таскивать PartialOrderReasoning (будет конфликтовать по begin/∎)
           Pe≤1 : ∀ e → P e ≤ 1#
           Pe≤1 e = proj₁ ≤-resp-≈  a₂ (e₁⊆e₂→Pe₁≤Pe₂ (e⊆Ω _))
+
+-- А вот так мы будем поступать, когда мне просто не хватает времени доказывать, но я твердо верю в то, что 
+-- утверждения верны.      
+record Consequences₂ (ax : Axioms) : Set where
+  open Axioms ax
+  field
+    -- Закон сложения  вероятностей
+    exclusion : ∀ e → P (Ω ∖ e) ≈ 1# - P e
+    P+P : ∀ e₁ e₂ → P (e₁ ∪ e₂) ≈  P e₁ + P e₂ - P (e₁ ∩ e₂)
+
+  open Axioms ax public
+  open Consequencses ax public