Documentation

BourbakiLean2.Order.Intervals

def Set.Ici {α : Type u_1} [Preorder α] (a : α) :

Set α

The interval [a, ∞).

Equations

Set.Ici a = {b : α | a ≤ b}

Instances For

def Set.Iic {α : Type u_1} [Preorder α] (a : α) :

Set α

The interval (-∞, a].

Equations

Set.Iic a = {b : α | b ≤ a}

Instances For

def Set.Ioi {α : Type u_1} [Preorder α] (a : α) :

Set α

The interval (a, ∞).

Equations

Set.Ioi a = {b : α | a < b}

Instances For

def Set.Iio {α : Type u_1} [Preorder α] (a : α) :

Set α

The interval (∞, a).

Equations

Set.Iio a = {b : α | b < a}

Instances For

def Set.Ioo {α : Type u_1} [Preorder α] (a b : α) :

Set α

The interval (a,b)

Equations

Set.Ioo a b = {c : α | a < c ∧ c < b}

Instances For

def Set.Ioc {α : Type u_1} [Preorder α] (a b : α) :

Set α

The interval (a,b]

Equations

Set.Ioc a b = {c : α | a < c ∧ c ≤ b}

Instances For

def Set.Ico {α : Type u_1} [Preorder α] (a b : α) :

Set α

The interval [a,b)

Equations

Set.Ico a b = {c : α | a ≤ c ∧ c < b}

Instances For

def Set.Icc {α : Type u_1} [Preorder α] (a b : α) :

Set α

The interval [a,b]

Equations

Set.Icc a b = {c : α | a ≤ c ∧ c ≤ b}

Instances For

mem interval iff

@[simp]

theorem Set.mem_Ici_iff {α : Type u_1} [Preorder α] {a b : α} :

b ∈ Set.Ici a ↔ a ≤ b

@[simp]

theorem Set.mem_Iic_iff {α : Type u_1} [Preorder α] {a b : α} :

b ∈ Set.Iic a ↔ b ≤ a

@[simp]

theorem Set.mem_Ioi_iff {α : Type u_1} [Preorder α] {a b : α} :

b ∈ Set.Ioi a ↔ a < b

@[simp]

theorem Set.mem_Iio_iff {α : Type u_1} [Preorder α] {a b : α} :

b ∈ Set.Iio a ↔ b < a

@[simp]

theorem Set.mem_Ioo_iff {α : Type u_1} [Preorder α] {a b c : α} :

c ∈ Set.Ioo a b ↔ a < c ∧ c < b

@[simp]

theorem Set.mem_Ioc_iff {α : Type u_1} [Preorder α] {a b c : α} :

c ∈ Set.Ioc a b ↔ a < c ∧ c ≤ b

@[simp]

theorem Set.mem_Ico_iff {α : Type u_1} [Preorder α] {a b c : α} :

c ∈ Set.Ico a b ↔ a ≤ c ∧ c < b

@[simp]

theorem Set.mem_Icc_iff {α : Type u_1} [Preorder α] {a b c : α} :

c ∈ Set.Icc a b ↔ a ≤ c ∧ c ≤ b

mem interval self

@[simp]

theorem Set.mem_Ici_self {α : Type u_1} [Preorder α] {a : α} :

a ∈ Set.Ici a

@[simp]

theorem Set.mem_Iic_self {α : Type u_1} [Preorder α] {a : α} :

a ∈ Set.Iic a

@[simp]

theorem Set.not_mem_Ioi_self {α : Type u_1} [Preorder α] {a : α} :

¬a ∈ Set.Ioi a

@[simp]

theorem Set.not_mem_Iio_self {α : Type u_1} [Preorder α] {a : α} :

¬a ∈ Set.Iio a

@[simp]

theorem Set.not_mem_Ioo_self_left {α : Type u_1} [Preorder α] {a b : α} :

¬a ∈ Set.Ioo a b

@[simp]

theorem Set.not_mem_Ioo_self_right {α : Type u_1} [Preorder α] {a b : α} :

¬b ∈ Set.Ioo a b

@[simp]

theorem Set.not_mem_Ioc_self_left {α : Type u_1} [Preorder α] {a b : α} :

¬a ∈ Set.Ioc a b

@[simp]

theorem Set.mem_Ioc_self_right_iff_lt {α : Type u_1} [Preorder α] {a b : α} :

b ∈ Set.Ioc a b ↔ a < b

@[simp]

theorem Set.mem_Ico_self_left_iff_lt {α : Type u_1} [Preorder α] {a b : α} :

a ∈ Set.Ico a b ↔ a < b

@[simp]

theorem Set.not_mem_Ico_self_right {α : Type u_1} [Preorder α] {a b : α} :

¬b ∈ Set.Ico a b

@[simp]

theorem Set.mem_Icc_self_left_iff_le {α : Type u_1} [Preorder α] {a b : α} :

a ∈ Set.Icc a b ↔ a ≤ b

@[simp]

theorem Set.mem_Icc_self_right_iff_le {α : Type u_1} [Preorder α] {a b : α} :

b ∈ Set.Icc a b ↔ a ≤ b

intersections

@[simp]

theorem Set.Ici_inter_Iic_eq_Icc {α : Type u_1} [Preorder α] {a b : α} :

Set.Ici a ∩ Set.Iic b = Set.Icc a b

[a,∞) ∩ (-∞,b] = [a,b]

@[simp]

theorem Set.Ioi_inter_Iic_eq_Ioc {α : Type u_1} [Preorder α] {a b : α} :

Set.Ioi a ∩ Set.Iic b = Set.Ioc a b

(a,∞] ∩ [-∞,b] = (a,b]

@[simp]

theorem Set.Ici_inter_Iio_eq_Ico {α : Type u_1} [Preorder α] {a b : α} :

Set.Ici a ∩ Set.Iio b = Set.Ico a b

[a,∞] ∩ [-∞,b) = [a,b)

@[simp]

theorem Set.Ioi_inter_Iio_eq_Ioo {α : Type u_1} [Preorder α] {a b : α} :

Set.Ioi a ∩ Set.Iio b = Set.Ioo a b

(a,∞] ∩ [-∞,b) = (a,b)

theorem Set.Ici_antitone {α : Type u_1} [Preorder α] :

Antitone Set.Ici

theorem Set.Ici_strictAnti {α : Type u_1} [Preorder α] :

StrictAntitone Set.Ici

theorem Set.Iic_monotone {α : Type u_1} [Preorder α] :

Monotone Set.Iic

theorem Set.Iic_strictMono {α : Type u_1} [Preorder α] :

StrictMonotone Set.Iic

empty iff

@[simp]

theorem Set.Icc_empty_iff_not_le {α : Type u_1} [PartialOrder α] {a b : α} :

Set.Icc a b = ∅ ↔ ¬a ≤ b

@[simp]

theorem Set.Ico_empty_iff_not_lt {α : Type u_1} [PartialOrder α] {a b : α} :

Set.Ico a b = ∅ ↔ ¬a < b

@[simp]

theorem Set.Ioc_empty_iff_not_lt {α : Type u_1} [PartialOrder α] {a b : α} :

Set.Ioc a b = ∅ ↔ ¬a < b

@[simp]

theorem Set.Ioi_empty_iff_maximum {α : Type u_1} [PartialOrder α] {a : α} :

Set.Ioi a = ∅ ↔ Maximal a

@[simp]

theorem Set.Iio_empty_iff_minimum {α : Type u_1} [PartialOrder α] {a : α} :

Set.Iio a = ∅ ↔ Minimal a

theorem Set.Ioi_antitone {α : Type u_1} [PartialOrder α] :

Antitone Set.Ioi

theorem Set.Ioi_strictAnti {α : Type u_1} [PartialOrder α] :

StrictAntitone Set.Ioi

theorem Set.Iio_monotone {α : Type u_1} [PartialOrder α] :

Monotone Set.Iio

theorem Set.Iio_strictAnti {α : Type u_1} [PartialOrder α] :

StrictMonotone Set.Iio

@[simp]

theorem Set.Ioi_union_point_eq_Ici {α : Type u_1} [PartialOrder α] {a : α} :

Set.Ioi a ∪ {a} = Set.Ici a

@[simp]

theorem Set.Iio_union_point_eq_Iic {α : Type u_1} [PartialOrder α] {a : α} :

Set.Iio a ∪ {a} = Set.Iic a

@[simp]

theorem Set.Ioo_union_point_eq_Ioc_of_lt {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) :

Set.Ioo a b ∪ {b} = Set.Ioc a b

@[simp]

theorem Set.Icc_self {α : Type u_1} [PartialOrder α] {a : α} :

Set.Icc a a = {a}

intersection theorems

@[simp]

theorem Set.Ici_inter_Ici {α : Type u_1} {a b : α} [SupSemilattice α] :

Set.Ici a ∩ Set.Ici b = Set.Ici (a ⊔ b)

@[simp]

theorem Set.Ici_inter_Icc {α : Type u_1} {a b c : α} [SupSemilattice α] :

Set.Ici a ∩ Set.Icc b c = Set.Icc (a ⊔ b) c

@[simp]

theorem Set.Ici_inter_Ico {α : Type u_1} {a b c : α} [SupSemilattice α] :

Set.Ici a ∩ Set.Ico b c = Set.Ico (a ⊔ b) c

@[simp]

theorem Set.Iic_inter_Iic {α : Type u_1} {a b : α} [InfSemilattice α] :

Set.Iic a ∩ Set.Iic b = Set.Iic (a ⊓ b)

@[simp]

theorem Set.Iic_inter_Ioc {α : Type u_1} {a b c : α} [InfSemilattice α] :

Set.Iic a ∩ Set.Ioc b c = Set.Ioc b (a ⊓ c)

@[simp]

theorem Set.Iic_inter_Icc {α : Type u_1} {a b c : α} [InfSemilattice α] :

Set.Iic a ∩ Set.Icc b c = Set.Icc b (a ⊓ c)

@[simp]

theorem Set.Icc_inter_Icc {α : Type u_1} {a b c d : α} [Lattice α] :

Set.Icc a b ∩ Set.Icc c d = Set.Icc (a ⊔ c) (b ⊓ d)

@[simp]

theorem Set.Ioi_inter_Ioi_of_le {α : Type u_1} {a b : α} [PartialOrder α] (h : a ≤ b) :

Set.Ioi a ∩ Set.Ioi b = Set.Ioi b

@[simp]

theorem Set.Ioi_inter_Ioi_of_ge {α : Type u_1} {a b : α} [PartialOrder α] (h : b ≤ a) :

Set.Ioi a ∩ Set.Ioi b = Set.Ioi a

@[simp]

theorem Set.Ioi_inter_Ioi_of_incomparable {α : Type u_1} {a b : α} [SupSemilattice α] (h : Incomparable a b) :

Set.Ioi a ∩ Set.Ioi b = Set.Ici (a ⊔ b)

@[simp]

theorem Set.Iio_inter_Iio_of_le {α : Type u_1} {a b : α} [PartialOrder α] (h : a ≤ b) :

Set.Iio a ∩ Set.Iio b = Set.Iio a

@[simp]

theorem Set.Iio_inter_Iio_of_ge {α : Type u_1} {a b : α} [PartialOrder α] (h : b ≤ a) :

Set.Iio a ∩ Set.Iio b = Set.Iio b

@[simp]

theorem Set.Iio_inter_Iio_of_incomparable {α : Type u_1} {a b : α} [InfSemilattice α] (h : Incomparable a b) :

Set.Iio a ∩ Set.Iio b = Set.Iic (a ⊓ b)

@[simp]

theorem Set.Iio_compl {α : Type u_1} {a : α} [TotalOrder α] :

(Set.Iio a)ᶜ = Set.Ici a

@[simp]

theorem Set.Ici_compl {α : Type u_1} {a : α} [TotalOrder α] :

(Set.Ici a)ᶜ = Set.Iio a

@[simp]

theorem Set.Iic_compl {α : Type u_1} {a : α} [TotalOrder α] :

(Set.Iic a)ᶜ = Set.Ioi a

@[simp]

theorem Set.Ioi_compl {α : Type u_1} {a : α} [TotalOrder α] :

(Set.Ioi a)ᶜ = Set.Iic a

theorem Set.iUnion_Iio_of_no_greatest {α : Type u_1} [TotalOrder α] (h : ∀ (a : α), ¬Greatest a) :

⋃ a : α, Set.Iio a = Set.univ

theorem Set.iUnion_Iio_of_greatest {α : Type u_1} {a : α} [TotalOrder α] (h : Greatest a) :

⋃ a : α, Set.Iio a = {a}ᶜ

@[simp]

theorem Set.Iio_subset_Iio_iff {α : Type u_1} {x y : α} [TotalOrder α] :

Set.Iio x ⊆ Set.Iio y ↔ x ≤ y

@[simp]

theorem Set.Ioi_subset_Ioi_iff {α : Type u_1} {x y : α} [TotalOrder α] :

Set.Ioi x ⊆ Set.Ioi y ↔ y ≤ x

@[simp]

theorem Set.Iio_subset_Iic {α : Type u_1} {x : α} [Preorder α] :

Set.Iio x ⊆ Set.Iic x

interval class

class Set.IsInterval {α : Type u_1} [Preorder α] (s : Set α) :

mem_of_mem_le_mem : ∀ {a b c : α}, a ≤ b → b ≤ c → a ∈ s → c ∈ s → b ∈ s

Instances

class Set.IsDownwardsClosed {α : Type u_1} [Preorder α] (s : Set α) :

mem_of_le_mem : ∀ {a b : α}, a ≤ b → b ∈ s → a ∈ s

Instances

class Set.IsUpwardsClosed {α : Type u_1} [Preorder α] (s : Set α) :

mem_of_mem_le : ∀ {a b : α}, a ≤ b → a ∈ s → b ∈ s

Instances

instance Set.instIsIntervalOfIsUpwardsClosed {α : Type u_1} [Preorder α] {s : Set α} [s.IsUpwardsClosed] :

s.IsInterval

Equations

⋯ = ⋯

instance Set.instIsIntervalOfIsDownwardsClosed {α : Type u_1} [Preorder α] {s : Set α} [s.IsDownwardsClosed] :

s.IsInterval

Equations

⋯ = ⋯

instance Set.instHasLeastSubtypeMemIci {α : Type u_1} [Preorder α] {a : α} :

HasLeast ↥(Set.Ici a)

Equations

Set.instHasLeastSubtypeMemIci = { least := ⟨a, ⋯⟩, least_le := ⋯ }

instance Set.instHasLeastSubtypeMemIcoOfLt {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :

HasLeast ↥(Set.Ico a b)

Equations

Set.instHasLeastSubtypeMemIcoOfLt h = { least := ⟨a, ⋯⟩, least_le := ⋯ }

instance Set.instHasLeastSubtypeMemIccOfLe {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) :

HasLeast ↥(Set.Icc a b)

Equations

Set.instHasLeastSubtypeMemIccOfLe h = { least := ⟨a, ⋯⟩, least_le := ⋯ }

instance Set.instHasGreatestSubtypeMemIic {α : Type u_1} [Preorder α] {a : α} :

HasGreatest ↥(Set.Iic a)

Equations

Set.instHasGreatestSubtypeMemIic = { greatest := ⟨a, ⋯⟩, le_greatest := ⋯ }

instance Set.instHasGreatestSubtypeMemIocOfLt {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :

HasGreatest ↥(Set.Ioc a b)

Equations

Set.instHasGreatestSubtypeMemIocOfLt h = { greatest := ⟨b, ⋯⟩, le_greatest := ⋯ }

instance Set.instHasGreatestSubtypeMemIccOfLe {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) :

HasGreatest ↥(Set.Icc a b)

Equations

Set.instHasGreatestSubtypeMemIccOfLe h = { greatest := ⟨b, ⋯⟩, le_greatest := ⋯ }

theorem Set.mem_of_mem_le_mem {α : Type u_1} [Preorder α] {a b c : α} {s : Set α} [s.IsInterval] (h : a ≤ b) (h' : b ≤ c) (ha : a ∈ s) (hc : c ∈ s) :

b ∈ s

theorem Set.mem_of_le_mem {α : Type u_1} [Preorder α] {s : Set α} [s.IsDownwardsClosed] {a b : α} (h : a ≤ b) (hb : b ∈ s) :

a ∈ s

theorem Set.mem_of_mem_le {α : Type u_1} [Preorder α] {s : Set α} [s.IsUpwardsClosed] {a b : α} (h : a ≤ b) (ha : a ∈ s) :

b ∈ s

instance Set.instIsUpwardsClosedIci {α : Type u_1} [Preorder α] {a : α} :

(Set.Ici a).IsUpwardsClosed

Equations

⋯ = ⋯

instance Set.instIsDownwardsClosedIic {α : Type u_1} [Preorder α] {a : α} :

(Set.Iic a).IsDownwardsClosed

Equations

⋯ = ⋯

instance Set.instIsUpwardsClosedIoi {α : Type u_1} [Preorder α] {a : α} :

(Set.Ioi a).IsUpwardsClosed

Equations

⋯ = ⋯

instance Set.instIsDownwardsClosedIio {α : Type u_1} [Preorder α] {a : α} :

(Set.Iio a).IsDownwardsClosed

Equations

⋯ = ⋯

instance Set.instIsIntervalIoo {α : Type u_1} [Preorder α] {a b : α} :

(Set.Ioo a b).IsInterval

Equations

⋯ = ⋯

instance Set.instIsIntervalIoc {α : Type u_1} [Preorder α] {a b : α} :

(Set.Ioc a b).IsInterval

Equations

⋯ = ⋯

instance Set.instIsIntervalIco {α : Type u_1} [Preorder α] {a b : α} :

(Set.Ico a b).IsInterval

Equations

⋯ = ⋯

instance Set.instIsIntervalIcc {α : Type u_1} [Preorder α] {a b : α} :

(Set.Icc a b).IsInterval

Equations

⋯ = ⋯

instance Set.instIsDownwardsClosedEmptyCollection {α : Type u_1} [Preorder α] :

∅.IsDownwardsClosed

Equations

⋯ = ⋯

instance Set.instIsUpwardsClosedEmptyCollection {α : Type u_1} [Preorder α] :

∅.IsUpwardsClosed

Equations

⋯ = ⋯

instance Set.instIsDownwardsClosedUniv {α : Type u_1} [Preorder α] :

Set.univ.IsDownwardsClosed

Equations

⋯ = ⋯

instance Set.instIsUpwardsClosedUniv {α : Type u_1} [Preorder α] :

Set.univ.IsUpwardsClosed

Equations

⋯ = ⋯

instance Set.instIsIntervalInter {α : Type u_1} [Preorder α] {s t : Set α} [s.IsInterval] [t.IsInterval] :

(s ∩ t).IsInterval

Equations

⋯ = ⋯

instance Set.instIsIntervalIInter {α : Type u_1} [Preorder α] {ι : Type u_2} {s : ι → Set α} [∀ (i : ι), (s i).IsInterval] :

(⋂ i : ι, s i).IsInterval

Equations

⋯ = ⋯

instance Set.instIsDownwardsClosedInter {α : Type u_1} [Preorder α] {s t : Set α} [s.IsDownwardsClosed] [t.IsDownwardsClosed] :

(s ∩ t).IsDownwardsClosed

Equations

⋯ = ⋯

instance Set.instIsDownwardsClosedIInter {α : Type u_1} [Preorder α] {ι : Type u_2} {s : ι → Set α} [∀ (i : ι), (s i).IsDownwardsClosed] :

(⋂ i : ι, s i).IsDownwardsClosed

Equations

⋯ = ⋯

instance Set.instIsUpwardsClosedInter {α : Type u_1} [Preorder α] {s t : Set α} [s.IsUpwardsClosed] [t.IsUpwardsClosed] :

(s ∩ t).IsUpwardsClosed

Equations

⋯ = ⋯

instance Set.instIsUpwardsClosedIInter {α : Type u_1} [Preorder α] {ι : Type u_2} {s : ι → Set α} [∀ (i : ι), (s i).IsUpwardsClosed] :

(⋂ i : ι, s i).IsUpwardsClosed

Equations

⋯ = ⋯

instance Set.instIsDownwardsClosedUnion {α : Type u_1} [Preorder α] {s t : Set α} [s.IsDownwardsClosed] [t.IsDownwardsClosed] :

(s ∪ t).IsDownwardsClosed

Equations

⋯ = ⋯

instance Set.IsDownwardsClosed.iUnion {α : Type u_1} [Preorder α] {ι : Type u_2} {s : ι → Set α} [∀ (i : ι), (s i).IsDownwardsClosed] :

(⋃ i : ι, s i).IsDownwardsClosed

Equations

⋯ = ⋯

instance Set.instIsUpwardsClosedUnion {α : Type u_1} [Preorder α] {s t : Set α} [s.IsUpwardsClosed] [t.IsUpwardsClosed] :

(s ∪ t).IsUpwardsClosed

Equations

⋯ = ⋯

instance Set.instIsUpwardsClosedIUnion {α : Type u_1} [Preorder α] {ι : Type u_2} {s : ι → Set α} [∀ (i : ι), (s i).IsUpwardsClosed] :

(⋃ i : ι, s i).IsUpwardsClosed

Equations

⋯ = ⋯

instance Set.instIsDownwardsClosedImageSubtypeMemVal {α : Type u_1} [Preorder α] {s : Set α} [s.IsDownwardsClosed] {t : Set ↥s} [t.IsDownwardsClosed] :

(Subtype.val '' t).IsDownwardsClosed

Equations

⋯ = ⋯

instance Set.instIsUpwardsClosedImageSubtypeMemVal {α : Type u_1} [Preorder α] {s : Set α} [s.IsUpwardsClosed] {t : Set ↥s} [t.IsUpwardsClosed] :

(Subtype.val '' t).IsUpwardsClosed

Equations

⋯ = ⋯

instance Set.instIsIntervalImageSubtypeMemVal {α : Type u_1} [Preorder α] {s : Set α} [s.IsInterval] {t : Set ↥s} [t.IsInterval] :

(Subtype.val '' t).IsInterval

Equations

⋯ = ⋯

instance Set.instIsIntervalSingleton {α : Type u_1} {a : α} [PartialOrder α] :

{a}.IsInterval

Equations

⋯ = ⋯

instance Set.downwards_has_least {α : Type} [Preorder α] {s : Set α} [s.IsDownwardsClosed] (h : s.Nonempty) [HasLeast α] :

Equations

Set.downwards_has_least h = { least := ⟨⊥, ⋯⟩, least_le := ⋯ }

instance Set.upwards_has_greatest {α : Type} [Preorder α] {s : Set α} [s.IsUpwardsClosed] (h : s.Nonempty) [HasGreatest α] :

HasGreatest ↥s

Equations

Set.upwards_has_greatest h = { greatest := ⟨⊤, ⋯⟩, le_greatest := ⋯ }