def «term_⊔_» : Lean.TrailingParserDescr

The maximum operation: max x y.

Equations

• «term_⊔_» = Lean.ParserDescr.trailingNode `«term_⊔_» 68 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊔ ") (Lean.ParserDescr.cat `term 69))

def «term_⊓_» : Lean.TrailingParserDescr

The minimum operation: min x y.

Equations

• «term_⊓_» = Lean.ParserDescr.trailingNode `«term_⊓_» 69 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊓ ") (Lean.ParserDescr.cat `term 70))

class InfSemilattice (α : Type u_2) extends PartialOrder α : Type u_2

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• inf : α → α → α
• inf_le_left : ∀ {x y : α}, InfSemilattice.inf x y ≤ x
• inf_le_right : ∀ {x y : α}, InfSemilattice.inf x y ≤ y
• le_inf_of : ∀ {x y z : α}, z ≤ x → z ≤ y → z ≤ InfSemilattice.inf x y

instance instMinOfInfSemilattice {α : Type u_1} [InfSemilattice α] : Min α

Equations

• instMinOfInfSemilattice = { min := InfSemilattice.inf }

theorem le_inf_of {α : Type u_1} [InfSemilattice α] {x y z : α} (h : z ≤ x) (h' : z ≤ y) : z ≤ x ⊓ y

@[simp]

theorem inf_le_left {α : Type u_1} [InfSemilattice α] {x y : α} : x ⊓ y ≤ x

@[simp]

theorem inf_le_right {α : Type u_1} [InfSemilattice α] {x y : α} : x ⊓ y ≤ y

instance instLeftDirected {α : Type u_1} [InfSemilattice α] : LeftDirected α

Equations

• ⋯ = ⋯

theorem inf_isGLB {α : Type u_1} [InfSemilattice α] {x y : α} : IsGLB {x, y} (x ⊓ y)

@[simp]

theorem inf_monotone_left {α : Type u_1} [InfSemilattice α] {x : α} : Monotone fun (y : α) => x ⊓ y

@[simp]

theorem inf_monotone_right {α : Type u_1} [InfSemilattice α] {y : α} : Monotone fun (x : α) => x ⊓ y

theorem inf_monotone {α : Type u_1} [InfSemilattice α] {x y z w : α} (h : x ≤ y) (h' : z ≤ w) : x ⊓ z ≤ y ⊓ w

@[simp]

theorem inf_self {α : Type u_1} [InfSemilattice α] {x : α} : x ⊓ x = x

@[simp]

theorem le_inf_iff {α : Type u_1} [InfSemilattice α] {x y z : α} : z ≤ x ⊓ y ↔ z ≤ x ∧ z ≤ y

theorem inf_comm {α : Type u_1} [InfSemilattice α] {x y : α} : x ⊓ y = y ⊓ x

theorem inf_assoc {α : Type u_1} [InfSemilattice α] {x y z : α} : x ⊓ (y ⊓ z) = x ⊓ y ⊓ z

@[simp]

theorem inf_eq_left_iff {α : Type u_1} [InfSemilattice α] {x y : α} : x ⊓ y = x ↔ x ≤ y

@[simp]

theorem inf_eq_right_iff {α : Type u_1} [InfSemilattice α] {x y : α} : x ⊓ y = y ↔ y ≤ x

class SupSemilattice (α : Type u_2) extends PartialOrder α : Type u_2

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left : ∀ {x y : α}, x ≤ SupSemilattice.sup x y
• le_sup_right : ∀ {x y : α}, y ≤ SupSemilattice.sup x y
• sup_le_of : ∀ {x y z : α}, x ≤ z → y ≤ z → SupSemilattice.sup x y ≤ z

instance instMaxOfSupSemilattice {α : Type u_1} [SupSemilattice α] : Max α

Equations

• instMaxOfSupSemilattice = { max := SupSemilattice.sup }

theorem sup_le_of {α : Type u_1} [SupSemilattice α] {x y z : α} (h : x ≤ z) (h' : y ≤ z) : x ⊔ y ≤ z

@[simp]

theorem le_sup_left {α : Type u_1} [SupSemilattice α] {x y : α} : x ≤ x ⊔ y

@[simp]

theorem le_sup_right {α : Type u_1} [SupSemilattice α] {x y : α} : y ≤ x ⊔ y

instance instRightDirected {α : Type u_1} [SupSemilattice α] : RightDirected α

Equations

• ⋯ = ⋯

theorem sup_isLUB {α : Type u_1} [SupSemilattice α] {x y : α} : IsLUB {x, y} (x ⊔ y)

@[simp]

theorem sup_monotone_left {α : Type u_1} [SupSemilattice α] {x : α} : Monotone fun (y : α) => x ⊔ y

@[simp]

theorem sup_monotone_right {α : Type u_1} [SupSemilattice α] {y : α} : Monotone fun (x : α) => x ⊔ y

theorem sup_monotone {α : Type u_1} [SupSemilattice α] {x y z w : α} (h : x ≤ y) (h' : z ≤ w) : x ⊔ z ≤ y ⊔ w

@[simp]

theorem sup_self {α : Type u_1} [SupSemilattice α] {x : α} : x ⊔ x = x

@[simp]

theorem sup_le_iff {α : Type u_1} [SupSemilattice α] {x y z : α} : x ⊔ y ≤ z ↔ x ≤ z ∧ y ≤ z

theorem sup_comm {α : Type u_1} [SupSemilattice α] {x y : α} : x ⊔ y = y ⊔ x

theorem sup_assoc {α : Type u_1} [SupSemilattice α] {x y z : α} : x ⊔ (y ⊔ z) = x ⊔ y ⊔ z

@[simp]

theorem sup_eq_left_iff {α : Type u_1} [SupSemilattice α] {x y : α} : x ⊔ y = x ↔ y ≤ x

@[simp]

theorem sup_eq_right_iff {α : Type u_1} [SupSemilattice α] {x y : α} : x ⊔ y = y ↔ x ≤ y

class Lattice (α : Type u_2) extends InfSemilattice α, SupSemilattice α : Type u_2

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• inf : α → α → α
• inf_le_left : ∀ {x y : α}, InfSemilattice.inf x y ≤ x
• inf_le_right : ∀ {x y : α}, InfSemilattice.inf x y ≤ y
• le_inf_of : ∀ {x y z : α}, z ≤ x → z ≤ y → z ≤ InfSemilattice.inf x y
• sup : α → α → α
• le_sup_left : ∀ {x y : α}, x ≤ Lattice.sup x y
• le_sup_right : ∀ {x y : α}, y ≤ Lattice.sup x y
• sup_le_of : ∀ {x y z : α}, x ≤ z → y ≤ z → Lattice.sup x y ≤ z

instance instLatticeSet {α : Type u_2} : Lattice (Set α)

Equations

• instLatticeSet = Lattice.mk (fun (x y : Set α) => x ∪ y) ⋯ ⋯ ⋯