Commit ee18ee95 authored by Michael Kohlhase's avatar Michael Kohlhase

comment is obsolete

parent 7cfafb8c
namespace http://mathhub.info/MitM/smglom/typedsets ❚
import base http://mathhub.info/MitM/Foundation ❚
// MiKo: failed to define an upset and downset ❚
theory UpDownSet : base:?Logic =
include ?POSet ❙
upset : {P : poset} (set (P.universe)) ⟶ bool ❘ = [P,F] ∀[x] ∀[y] x ∈ F ∧ (P.ord) x y ⇒ y ∈ F ❘ # upset 2❙
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment