Interval subposets
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-03-17.
Last modified on 2023-05-07.
module order-theory.interval-subposets where
Imports
open import foundation.propositions open import foundation.universe-levels open import order-theory.posets open import order-theory.subposets
Idea
Given two elements x
and y
in a poset X
, the interval subposet
[x, y]
is the subposet of X
consisting of all elements z
in X
such that
x ≤ z
and z ≤ y
. Note that interval subposets need not be linearly ordered.
Definition
module _ {l1 l2 : Level} (X : Poset l1 l2) (x y : type-Poset X) where is-in-interval-Poset : (z : type-Poset X) → Prop l2 is-in-interval-Poset z = prod-Prop (leq-Poset-Prop X x z) (leq-Poset-Prop X z y) poset-interval-Subposet : Poset (l1 ⊔ l2) l2 poset-interval-Subposet = poset-Subposet X is-in-interval-Poset
Recent changes
- 2023-05-07. Egbert Rijke. Cleaning up order theory some more (#599).
- 2023-05-05. Egbert Rijke. Cleaning up order theory 3 (#593).
- 2023-05-05. Egbert Rijke. cleaning up order theory (#591).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).