From bc7d4ca9c26d2bf07986653b37d2a2a1d4c3e439 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 1 Jun 2016 13:45:40 +0200 Subject: [PATCH] =?UTF-8?q?Notations=20for=20X=20=E2=8A=86=20Y=20=E2=8A=86?= =?UTF-8?q?=20Z.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- theories/base.v | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/theories/base.v b/theories/base.v index 22752705..bfcb09ae 100644 --- a/theories/base.v +++ b/theories/base.v @@ -637,6 +637,11 @@ Notation "(⊄)" := (λ X Y, X ⊄ Y) (only parsing) : C_scope. Notation "( X ⊄ )" := (λ Y, X ⊄ Y) (only parsing) : C_scope. Notation "( ⊄ X )" := (λ Y, Y ⊄ X) (only parsing) : C_scope. +Notation "X ⊆ Y ⊆ Z" := (X ⊆ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : C_scope. +Notation "X ⊆ Y ⊂ Z" := (X ⊆ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : C_scope. +Notation "X ⊂ Y ⊆ Z" := (X ⊂ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : C_scope. +Notation "X ⊂ Y ⊂ Z" := (X ⊂ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : C_scope. + (** The class [Lexico A] is used for the lexicographic order on [A]. This order is used to create finite maps, finite sets, etc, and is typically different from the order [(⊆)]. *) -- GitLab