case h_cobounded.a
ι : Type ?u.6300
α : Type u_1
β : Type ?u.6306
t t' : Bornology α
h : ∀ (s : Set α), IsBounded s ↔ IsBounded s
s : Set α
⊢ s ∈ cobounded α ↔ s ∈ cobounded α
ι : Type ?u.6300
α : Type u_1
β : Type ?u.6306
t t' : Bornology α
h : ∀ (s : Set α), IsBounded s ↔ IsBounded s
⊢ t = t'
ext s
no goals
case h_cobounded.a
ι : Type ?u.6300
α : Type u_1
β : Type ?u.6306
t t' : Bornology α
h : ∀ (s : Set α), IsBounded s ↔ IsBounded s
s : Set α
⊢ s ∈ cobounded α ↔ s ∈ cobounded α
simpa [@isBounded_def _ t, isBounded_def, compl_compl] using h (sᶜ)