Documentation

Mathlib.Order.UpperLower.Prod

Upper and lower set product #

The Cartesian product of sets carries over to upper and lower sets in a natural way. This file defines said product over the types UpperSet and LowerSet and proves some of its properties.

Notation #

source
theorem IsUpperSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : IsUpperSet s) (ht : IsUpperSet t) :
IsUpperSet (s ×ˢ t)
source
theorem IsLowerSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : IsLowerSet s) (ht : IsLowerSet t) :
IsLowerSet (s ×ˢ t)
source
def UpperSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t : UpperSet β) :
UpperSet (α × β)

The product of two upper sets as an upper set.

Equations
    Instances For
      source
      instance UpperSet.instSProd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
      SProd (UpperSet α) (UpperSet β) (UpperSet (α × β))
      Equations
        source
        @[simp]
        theorem UpperSet.coe_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t : UpperSet β) :
        ↑(s ×ˢ t) = ↑s ×ˢ ↑t
        source
        @[simp]
        theorem UpperSet.mem_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} {s : UpperSet α} {t : UpperSet β} :
        x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t
        source
        theorem UpperSet.Ici_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (x : α × β) :
        Ici x = Ici x.1 ×ˢ Ici x.2
        source
        @[simp]
        theorem UpperSet.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) :
        Ici a ×ˢ Ici b = Ici (a, b)
        source
        @[simp]
        theorem UpperSet.prod_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) :
        s ×ˢ ⊤ = ⊤
        source
        @[simp]
        theorem UpperSet.top_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (t : UpperSet β) :
        ⊤ ×ˢ t = ⊤
        source
        @[simp]
        theorem UpperSet.bot_prod_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
        ⊥ ×ˢ ⊥ = ⊥
        source
        @[simp]
        theorem UpperSet.sup_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ s₂ : UpperSet α) (t : UpperSet β) :
        (s₁ ⊔ s₂) ×ˢ t = s₁ ×ˢ t ⊔ s₂ ×ˢ t
        source
        @[simp]
        theorem UpperSet.prod_sup {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t₁ t₂ : UpperSet β) :
        s ×ˢ (t₁ ⊔ t₂) = s ×ˢ t₁ ⊔ s ×ˢ t₂
        source
        @[simp]
        theorem UpperSet.inf_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ s₂ : UpperSet α) (t : UpperSet β) :
        (s₁ ⊓ s₂) ×ˢ t = s₁ ×ˢ t ⊓ s₂ ×ˢ t
        source
        @[simp]
        theorem UpperSet.prod_inf {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t₁ t₂ : UpperSet β) :
        s ×ˢ (t₁ ⊓ t₂) = s ×ˢ t₁ ⊓ s ×ˢ t₂
        source
        theorem UpperSet.prod_sup_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ s₂ : UpperSet α) (t₁ t₂ : UpperSet β) :
        s₁ ×ˢ t₁ ⊔ s₂ ×ˢ t₂ = (s₁ ⊔ s₂) ×ˢ (t₁ ⊔ t₂)
        source
        theorem UpperSet.prod_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : UpperSet α} {t₁ t₂ : UpperSet β} :
        s₁ ≤ s₂ → t₁ ≤ t₂ → s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂
        source
        theorem UpperSet.prod_mono_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : UpperSet α} {t : UpperSet β} :
        s₁ ≤ s₂ → s₁ ×ˢ t ≤ s₂ ×ˢ t
        source
        theorem UpperSet.prod_mono_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : UpperSet α} {t₁ t₂ : UpperSet β} :
        t₁ ≤ t₂ → s ×ˢ t₁ ≤ s ×ˢ t₂
        source
        @[simp]
        theorem UpperSet.prod_self_le_prod_self {α : Type u_1} [Preorder α] {s₁ s₂ : UpperSet α} :
        s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂
        source
        @[simp]
        theorem UpperSet.prod_self_lt_prod_self {α : Type u_1} [Preorder α] {s₁ s₂ : UpperSet α} :
        s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂
        source
        theorem UpperSet.prod_le_prod_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : UpperSet α} {t₁ t₂ : UpperSet β} :
        s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₂ = ⊤ ∨ t₂ = ⊤
        source
        @[simp]
        theorem UpperSet.prod_eq_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : UpperSet α} {t : UpperSet β} :
        s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤
        source
        @[simp]
        theorem UpperSet.codisjoint_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : UpperSet α} {t₁ t₂ : UpperSet β} :
        Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂
        source
        def LowerSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t : LowerSet β) :
        LowerSet (α × β)

        The product of two lower sets as a lower set.

        Equations
          Instances For
            source
            instance LowerSet.instSProd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
            SProd (LowerSet α) (LowerSet β) (LowerSet (α × β))
            Equations
              source
              @[simp]
              theorem LowerSet.coe_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t : LowerSet β) :
              ↑(s ×ˢ t) = ↑s ×ˢ ↑t
              source
              @[simp]
              theorem LowerSet.mem_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} {s : LowerSet α} {t : LowerSet β} :
              x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t
              source
              theorem LowerSet.Iic_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (x : α × β) :
              Iic x = Iic x.1 ×ˢ Iic x.2
              source
              @[simp]
              theorem LowerSet.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) :
              Iic a ×ˢ Iic b = Iic (a, b)
              source
              @[simp]
              theorem LowerSet.prod_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) :
              s ×ˢ ⊥ = ⊥
              source
              @[simp]
              theorem LowerSet.bot_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (t : LowerSet β) :
              ⊥ ×ˢ t = ⊥
              source
              @[simp]
              theorem LowerSet.top_prod_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
              ⊤ ×ˢ ⊤ = ⊤
              source
              @[simp]
              theorem LowerSet.inf_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ s₂ : LowerSet α) (t : LowerSet β) :
              (s₁ ⊓ s₂) ×ˢ t = s₁ ×ˢ t ⊓ s₂ ×ˢ t
              source
              @[simp]
              theorem LowerSet.prod_inf {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t₁ t₂ : LowerSet β) :
              s ×ˢ (t₁ ⊓ t₂) = s ×ˢ t₁ ⊓ s ×ˢ t₂
              source
              @[simp]
              theorem LowerSet.sup_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ s₂ : LowerSet α) (t : LowerSet β) :
              (s₁ ⊔ s₂) ×ˢ t = s₁ ×ˢ t ⊔ s₂ ×ˢ t
              source
              @[simp]
              theorem LowerSet.prod_sup {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t₁ t₂ : LowerSet β) :
              s ×ˢ (t₁ ⊔ t₂) = s ×ˢ t₁ ⊔ s ×ˢ t₂
              source
              theorem LowerSet.prod_inf_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ s₂ : LowerSet α) (t₁ t₂ : LowerSet β) :
              s₁ ×ˢ t₁ ⊓ s₂ ×ˢ t₂ = (s₁ ⊓ s₂) ×ˢ (t₁ ⊓ t₂)
              source
              theorem LowerSet.prod_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : LowerSet α} {t₁ t₂ : LowerSet β} :
              s₁ ≤ s₂ → t₁ ≤ t₂ → s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂
              source
              theorem LowerSet.prod_mono_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : LowerSet α} {t : LowerSet β} :
              s₁ ≤ s₂ → s₁ ×ˢ t ≤ s₂ ×ˢ t
              source
              theorem LowerSet.prod_mono_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {t₁ t₂ : LowerSet β} :
              t₁ ≤ t₂ → s ×ˢ t₁ ≤ s ×ˢ t₂
              source
              @[simp]
              theorem LowerSet.prod_self_le_prod_self {α : Type u_1} [Preorder α] {s₁ s₂ : LowerSet α} :
              s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂
              source
              @[simp]
              theorem LowerSet.prod_self_lt_prod_self {α : Type u_1} [Preorder α] {s₁ s₂ : LowerSet α} :
              s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂
              source
              theorem LowerSet.prod_le_prod_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : LowerSet α} {t₁ t₂ : LowerSet β} :
              s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₁ = ⊥ ∨ t₁ = ⊥
              source
              @[simp]
              theorem LowerSet.prod_eq_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {t : LowerSet β} :
              s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥
              source
              @[simp]
              theorem LowerSet.disjoint_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ s₂ : LowerSet α} {t₁ t₂ : LowerSet β} :
              Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
              source
              @[simp]
              theorem upperClosure_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : Set α) (t : Set β) :
              upperClosure (s ×ˢ t) = upperClosure s ×ˢ upperClosure t
              source
              @[simp]
              theorem lowerClosure_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : Set α) (t : Set β) :
              lowerClosure (s ×ˢ t) = lowerClosure s ×ˢ lowerClosure t