α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : SemilatticeInf α
inst✝ : Nonempty α
s : Set α
⊢ ¬Set.Infinite s → BddBelow s
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : SemilatticeInf α
inst✝ : Nonempty α
s : Set α
⊢ ¬BddBelow s → Set.Infinite s
contrapose!
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : SemilatticeInf α
inst✝ : Nonempty α
s : Set α
⊢ Set.Finite s → BddBelow s
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : SemilatticeInf α
inst✝ : Nonempty α
s : Set α
⊢ ¬Set.Infinite s → BddBelow s
rw [not_infinite]
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : SemilatticeInf α
inst✝ : Nonempty α
s : Set α
⊢ Set.Finite s → BddBelow s
exact Finite.bddBelow