α : Type u_2
ι : Sort ?u.24409
κ : ι → Sort ?u.24414
β : Type u_1
inst✝ : SetLike α β
l : LowerAdjoint SetLike.coe
s : Set β
x : β
⊢ toFun l {x} ≤ toFun l s ↔ ∀ (S : α), toFun l s ≤ S → toFun l {x} ≤ S
α : Type u_2
ι : Sort ?u.24409
κ : ι → Sort ?u.24414
β : Type u_1
inst✝ : SetLike α β
l : LowerAdjoint SetLike.coe
s : Set β
x : β
⊢ x ∈ toFun l s ↔ ∀ (S : α), s ⊆ ↑S → x ∈ S
simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← l.le_iff_subset]
no goals
α : Type u_2
ι : Sort ?u.24409
κ : ι → Sort ?u.24414
β : Type u_1
inst✝ : SetLike α β
l : LowerAdjoint SetLike.coe
s : Set β
x : β
⊢ toFun l {x} ≤ toFun l s ↔ ∀ (S : α), toFun l s ≤ S → toFun l {x} ≤ S
exact ⟨fun h S => h.trans, fun h => h _ le_rfl⟩