α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) → Bounded (fun x x_1 => x ≤ x_1) s
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) ↔ Bounded (fun x x_1 => x ≤ x_1) s
refine' ⟨_, Bounded.mono (Set.inter_subset_left s _)⟩
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) → Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a < b})
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) → Bounded (fun x x_1 => x ≤ x_1) s
rw [← @bounded_le_inter_lt _ s _ a]
no goals
α : Type u_1
r : α → α → Prop
s t : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) → Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a < b})
exact Bounded.mono fun x ⟨hx, hx'⟩ => ⟨hx, le_of_lt hx'⟩