case intro
α : Type u_2
β : Type u_1
γ : Type ?u.11552
ι : Type ?u.11555
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x x_1 => x ≤ x_1) x b
⊢ BddAbove (range f)
α : Type u_2
β : Type u_1
γ : Type ?u.11552
ι : Type ?u.11555
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) cofinite f
⊢ BddAbove (range f)
rcases hf with ⟨b, hb⟩
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.11552
ι : Type ?u.11555
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x x_1 => x ≤ x_1) x b
this : Nonempty β
⊢ BddAbove (range f)
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.11552
ι : Type ?u.11555
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x x_1 => x ≤ x_1) x b
⊢ BddAbove (range f)
haveI : Nonempty β := ⟨b⟩
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.11552
ι : Type ?u.11555
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x x_1 => x ≤ x_1) x b
this : Nonempty β
⊢ BddAbove (f '' {x | f x ≤ b}) ∧ BddAbove (f '' {x | f x ≤ b}ᶜ)
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.11552
ι : Type ?u.11555
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x x_1 => x ≤ x_1) x b
this : Nonempty β
⊢ BddAbove (range f)
rw [← image_univ, ← union_compl_self { x | f x ≤ b }, image_union, bddAbove_union]
no goals
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.11552
ι : Type ?u.11555
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x x_1 => x ≤ x_1) x b
this : Nonempty β
⊢ BddAbove (f '' {x | f x ≤ b}) ∧ BddAbove (f '' {x | f x ≤ b}ᶜ)
exact ⟨⟨b, ball_image_iff.2 fun x => id⟩, (hb.image f).bddAbove⟩