def IsGLB {α : Type u_1} [Preorder α] (s : Set α) (a : α) : Prop

Equations

• IsGLB s a = ∃ (h : LowerBound s a), Greatest ⟨a, h⟩

def IsLUB {α : Type u_1} [Preorder α] (s : Set α) (a : α) : Prop

Equations

• IsLUB s a = ∃ (h : UpperBound s a), Least ⟨a, h⟩

def IsGLBi {α : Type u_1} {ι : Type u_2} [Preorder α] (x : ι → α) (a : α) : Prop

Equations

• IsGLBi x = IsGLB (x '' Set.univ)

def IsLUBi {α : Type u_1} {ι : Type u_2} [Preorder α] (x : ι → α) (a : α) : Prop

Equations

• IsLUBi x = IsLUB (x '' Set.univ)

theorem isGLB_iff {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsGLB s a ↔ LowerBound s a ∧ ∀ (b : α), LowerBound s b → b ≤ a

theorem isLUB_iff {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsLUB s a ↔ UpperBound s a ∧ ∀ (b : α), UpperBound s b → a ≤ b

theorem isGLBi_iff {α : Type u_1} [Preorder α] {a : α} {ι : Type u_2} {x : ι → α} : IsGLBi x a ↔ (∀ (i : ι), a ≤ x i) ∧ ∀ (b : α), (∀ (i : ι), b ≤ x i) → b ≤ a

theorem isLUBi_iff {α : Type u_1} [Preorder α] {a : α} {ι : Type u_2} {x : ι → α} : IsLUBi x a ↔ (∀ (i : ι), x i ≤ a) ∧ ∀ (b : α), (∀ (i : ι), x i ≤ b) → a ≤ b

theorem Least.isGLB_of_mem {α : Type u_1} [Preorder α] {s : Set α} {a : ↥s} (h : Least a) : IsGLB s a.val

theorem Greatest.isLUB_of_mem {α : Type u_1} [Preorder α] {s : Set α} {a : ↥s} (h : Greatest a) : IsLUB s a.val

@[simp]

theorem op_isGLB_iff {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsGLB s (toOp a) ↔ IsLUB s a

@[simp]

theorem op_isLUB_iff {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsLUB s (toOp a) ↔ IsGLB s a

@[simp]

theorem isGLB_empty_iff_greatest {α : Type u_1} [Preorder α] {a : α} : IsGLB ∅ a ↔ Greatest a

@[simp]

theorem isLUB_empty_iff_least {α : Type u_1} [Preorder α] {a : α} : IsLUB ∅ a ↔ Least a

theorem isGLB_le_isLUB {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : s.Nonempty) (ha : IsGLB s a) (hb : IsLUB s b) : a ≤ b

theorem IsGLB.le {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : IsGLB s a) (h' : b ∈ s) : a ≤ b

theorem IsLUB.ge {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : IsLUB s a) (h' : b ∈ s) : b ≤ a

theorem IsGLBi.le {α : Type u_1} [Preorder α] {a : α} {ι : Type u_2} {x : ι → α} {i : ι} (h : IsGLBi x a) : a ≤ x i

theorem IsLUBi.ge {α : Type u_1} [Preorder α] {a : α} {ι : Type u_2} {x : ι → α} {i : ι} (h : IsLUBi x a) : x i ≤ a

@[simp]

theorem IsGLB.ge_iff {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : IsGLB s a) : b ≤ a ↔ ∀ (x : α), x ∈ s → b ≤ x

@[simp]

theorem IsLUB.le_iff {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : IsLUB s a) : a ≤ b ↔ ∀ (x : α), x ∈ s → x ≤ b

theorem IsGLBi.ge_iff {α : Type u_1} [Preorder α] {a b : α} {ι : Type u_2} {x : ι → α} (h : IsGLBi x a) : b ≤ a ↔ ∀ (i : ι), b ≤ x i

theorem IsLUBi.le_iff {α : Type u_1} [Preorder α] {a b : α} {ι : Type u_2} {x : ι → α} (h : IsLUBi x a) : a ≤ b ↔ ∀ (i : ι), x i ≤ b

theorem isGLB_antitone {α : Type u_1} [Preorder α] {s t : Set α} {a b : α} (h : s ⊆ t) (h' : IsGLB s a) (h'' : IsGLB t b) : b ≤ a

theorem isLUB_monotone {α : Type u_1} [Preorder α] {s t : Set α} {a b : α} (h : s ⊆ t) (h' : IsLUB s a) (h'' : IsLUB t b) : a ≤ b

theorem isGLBi_index_subset {α : Type u_1} [Preorder α] {a b : α} {ι : Type u_2} {x : ι → α} {r : Set ι} (h' : IsGLBi x a) (h'' : IsGLBi (x ∘ Subtype.val) b) : a ≤ b

theorem isLUBi_index_subset {α : Type u_1} [Preorder α] {a b : α} {ι : Type u_2} {x : ι → α} {r : Set ι} (h' : IsLUBi x a) (h'' : IsLUBi (x ∘ Subtype.val) b) : b ≤ a

theorem isGLBi_monotone {α : Type u_1} [Preorder α] {a b : α} {ι : Type u_2} {x x' : ι → α} (h : ∀ (i : ι), x i ≤ x' i) (h' : IsGLBi x a) (h'' : IsGLBi x' b) : a ≤ b

theorem isLUBi_monotone {α : Type u_1} [Preorder α] {a b : α} {ι : Type u_2} {x x' : ι → α} (h : ∀ (i : ι), x i ≤ x' i) (h' : IsLUBi x a) (h'' : IsLUBi x' b) : a ≤ b

theorem isLUBi_covering_iff {α : Type u_1} [Preorder α] {b : α} {ι : Type u_2} {x : ι → α} {ι' : Type u_3} {j : ι' → Set ι} {a : ι' → α} (h : Set.IsCovering j) (h' : ∀ (i' : ι'), IsLUBi (x|_j i') (a i')) : IsLUBi x b ↔ IsLUBi a b

theorem isGLBi_covering_iff {α : Type u_1} [Preorder α] {b : α} {ι : Type u_2} {x : ι → α} {ι' : Type u_3} {j : ι' → Set ι} {a : ι' → α} (h : Set.IsCovering j) (h' : ∀ (i' : ι'), IsGLBi (x|_j i') (a i')) : IsGLBi x b ↔ IsGLBi a b

theorem isLUBi_double_family {α : Type u_1} [Preorder α] {ι : Type u_2} {ι' : Type} {x : ι' → ι → α} {a : ι' → α} {b : α} (h : ∀ (i' : ι'), IsLUBi (x i') (a i')) : IsLUBi (Function.uncurry x) b ↔ IsLUBi a b

theorem isGLBi_double_family {α : Type u_1} [Preorder α] {ι : Type u_2} {ι' : Type} {x : ι' → ι → α} {a : ι' → α} {b : α} (h : ∀ (i' : ι'), IsGLBi (x i') (a i')) : IsGLBi (Function.uncurry x) b ↔ IsGLBi a b

theorem isLUB_pointwise {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Preorder (α i)] (x : Set ((i : ι) → α i)) (a : (i : ι) → α i) : IsLUB x a ↔ ∀ (i : ι), IsLUB ((fun (p : (i : ι) → α i) => p i) '' x) (a i)

theorem isGLB_pointwise {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Preorder (α i)] (x : Set ((i : ι) → α i)) (a : (i : ι) → α i) : IsGLB x a ↔ ∀ (i : ι), IsGLB ((fun (p : (i : ι) → α i) => p i) '' x) (a i)

theorem IsLUB.in_ambient_le_in_subset {α : Type u_1} [Preorder α] {s : Set α} {t : Set ↥s} {a : ↥s} {a' : α} (h : IsLUB t a) (h' : IsLUB (Subtype.val '' t) a') : a' ≤ a.val

theorem IsGLB.in_subset_le_in_ambient {α : Type u_1} [Preorder α] {s : Set α} {t : Set ↥s} {a : ↥s} {a' : α} (h : IsGLB t a) (h' : IsGLB (Subtype.val '' t) a') : a.val ≤ a'

theorem IsLUB.same_in_subset {α : Type u_1} [Preorder α] {s : Set α} {t : Set ↥s} {a : ↥s} (h : IsLUB (Subtype.val '' t) a.val) : IsLUB t a

theorem IsGLB.same_in_subset {α : Type u_1} [Preorder α] {s : Set α} {t : Set ↥s} {a : ↥s} (h : IsGLB (Subtype.val '' t) a.val) : IsGLB t a

theorem IsGLB.all_eq {α : Type u_3} [PartialOrder α] {s : Set α} {a b : α} (h : IsGLB s a) (h' : IsGLB s b) : a = b

theorem IsLUB.all_eq {α : Type u_3} [PartialOrder α] {s : Set α} {a b : α} (h : IsLUB s a) (h' : IsLUB s b) : a = b

instance instSubsingletonSubtypeIsGLB {α : Type u_3} [PartialOrder α] {s : Set α} : Subsingleton { a : α // IsGLB s a }

Equations

• ⋯ = ⋯

instance instSubsingletonSubtypeIsLUB {α : Type u_3} [PartialOrder α] {s : Set α} : Subsingleton { a : α // IsLUB s a }

Equations

• ⋯ = ⋯

@[simp]

theorem isGLB_singleton_iff_eq {α : Type u_3} [PartialOrder α] {a a' : α} : IsGLB {a} a' ↔ a = a'

@[simp]

theorem isLUB_singleton_iff_eq {α : Type u_3} [PartialOrder α] {a a' : α} : IsLUB {a} a' ↔ a = a'