α : Type u_1
β : Type ?u.20383
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → c ≤ a → c ≤ b
⊢ sSup {a_1 | IsAtom a_1 ∧ a_1 ≤ a} ≤ sSup {a | IsAtom a ∧ a ≤ b}
α : Type u_1
β : Type ?u.20383
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → c ≤ a → c ≤ b
⊢ a ≤ b
rw [← sSup_atoms_le_eq a, ← sSup_atoms_le_eq b]
no goals
α : Type u_1
β : Type ?u.20383
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → c ≤ a → c ≤ b
⊢ sSup {a_1 | IsAtom a_1 ∧ a_1 ≤ a} ≤ sSup {a | IsAtom a ∧ a ≤ b}
exact sSup_le_sSup fun c hc => ⟨hc.1, h c hc.1 hc.2⟩