Commits

ppavel  committed b2dfcce

⊆ для событий (получен из poset для решеток)

  • Participants
  • Parent commits 237cccc

Comments (0)

Files changed (2)

File EventAlgebra.agda

     _∖_ : Op₂ Event
     a ∖ b = a ∩ ∁ b
     
---    _⊆_ : Rel Event zero
---    e₁ ⊆ e₂ = {!!}
-
   _disj_ : Rel Event zero
   e₁ disj e₂ = e₁ ∩ e₂ ≈ ∅
 
       Carrier = Event; _≈_ = _≈_; _∙_ = _∪_; ε = ∅; 
       isMonoid = IsCommutativeSemiring.+-isMonoid (B.∨-∧-isCommutativeSemiring algebra) }
 
+  open Poset (B.poset algebra) public using () renaming (_≤_ to _⊆_)
+
  

File Probability.agda

     a₂ : P Ω ≈ 1#
     a₃ : ∀{l} → Disjoint l → P (∪ l) ≈ Σ (map P l)
      
--- e₁⊆e₂→Pe₁≤Pe₂ : ∀ {e₁ e₂ } → e₁ ⊆ e₂ → P e₁ ≤ P e₂
--- e₁⊆e₂→Pe₁≤Pe₂ = {!-m!}
+  e₁⊆e₂→Pe₁≤Pe₂ : ∀ {e₁ e₂ } → e₁ ⊆ e₂ → P e₁ ≤ P e₂
+  e₁⊆e₂→Pe₁≤Pe₂ = {!-m!}