/-
Copyright (c) 2022 Jireh Loreaux. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jireh Loreaux

! This file was ported from Lean 3 source module topology.bornology.basic
! leanprover-community/mathlib commit 8631e2d5ea77f6c13054d9151d82b83069680cb1
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.Filter.Cofinite

/-!
# Basic theory of bornology

We develop the basic theory of bornologies. Instead of axiomatizing bounded sets and defining
bornologies in terms of those, we recognize that the cobounded sets form a filter and define a
bornology as a filter of cobounded sets which contains the cofinite filter.  This allows us to make
use of the extensive library for filters, but we also provide the relevant connecting results for
bounded sets.

The specification of a bornology in terms of the cobounded filter is equivalent to the standard
one (e.g., see [Bourbaki, *Topological Vector Spaces*][bourbaki1987], **covering bornology**, now
often called simply **bornology**) in terms of bounded sets (see `Bornology.ofBounded`,
`IsBounded.union`, `IsBounded.subset`), except that we do not allow the empty bornology (that is,
we require that *some* set must be bounded; equivalently, `∅` is bounded). In the literature the
cobounded filter is generally referred to as the *filter at infinity*.

## Main definitions

- `Bornology α`: a class consisting of `cobounded : Filter α` and a proof that this filter
  contains the `cofinite` filter.
- `Bornology.IsCobounded`: the predicate that a set is a member of the `cobounded α` filter. For
  `s : Set α`, one should prefer `Bornology.IsCobounded s` over `s ∈ cobounded α`.
- `bornology.IsBounded`: the predicate that states a set is bounded (i.e., the complement of a
  cobounded set). One should prefer `Bornology.IsBounded s` over `sᶜ ∈ cobounded α`.
- `BoundedSpace α`: a class extending `Bornology α` with the condition
  `Bornology.IsBounded (Set.univ : Set α)`

Although use of `cobounded α` is discouraged for indicating the (co)boundedness of individual sets,
it is intended for regular use as a filter on `α`.
-/


open Set Filter

variable {ι: Type ?u.2
ι α: Type ?u.6236
α β: Type ?u.8
β : Type _: Type (?u.10045+1)
Type _}

/-- A **bornology** on a type `α` is a filter of cobounded sets which contains the cofinite filter.
Such spaces are equivalently specified by their bounded sets, see `Bornology.ofBounded`
and `Bornology.ext_iff_isBounded`-/
class Bornology: Type u_1 → Type u_1
Bornology (α: Type ?u.20
α : Type _: Type (?u.20+1)
Type _) where
  /-- The filter of cobounded sets in a bornology. This is a field of the structure, but one
  should always prefer `Bornology.cobounded` because it makes the `α` argument explciit. -/
  cobounded': {α : Type u_1} → [self : Bornology α] → Filter α
cobounded' : Filter: Type ?u.25 → Type ?u.25
Filter α: Type ?u.20
α
  /-- The cobounded filter in a bornology is smaller than the cofinite filter. This is a field of
  the structure, but one should always prefer `Bornology.le_cofinite` because it makes the `α`
  argument explciit. -/
  le_cofinite': ∀ {α : Type u_1} [self : Bornology α], Bornology.cobounded' ≤ cofinite
le_cofinite' : cobounded': Filter α
cobounded' ≤ cofinite: {α : Type ?u.29} → Filter α
cofinite
#align bornology Bornology: Type u_1 → Type u_1
Bornology

/- porting note: Because Lean 4 doesn't accept the `[]` syntax to make arguments of structure
fields explicit, we have to define these separately, prove the `ext` lemmas manually, and
initialize new `simps` projections. -/

/-- The filter of cobounded sets in a bornology. -/
def Bornology.cobounded: (α : Type ?u.111) → [inst : Bornology α] → Filter α
Bornology.cobounded (α: Type ?u.111
α : Type _: Type (?u.111+1)
Type _) [Bornology: Type ?u.114 → Type ?u.114
Bornology α: Type ?u.111
α] : Filter: Type ?u.117 → Type ?u.117
Filter α: Type ?u.111
α := Bornology.cobounded': {α : Type ?u.121} → [self : Bornology α] → Filter α
Bornology.cobounded'
#align bornology.cobounded Bornology.cobounded: (α : Type u_1) → [inst : Bornology α] → Filter α
Bornology.cobounded

alias Bornology.cobounded: (α : Type u_1) → [inst : Bornology α] → Filter α
Bornology.cobounded ← Bornology.Simps.cobounded: (α : Type u_1) → [inst : Bornology α] → Filter α
Bornology.Simps.cobounded

lemma Bornology.le_cofinite: ∀ (α : Type u_1) [inst : Bornology α], cobounded α ≤ cofinite
Bornology.le_cofinite (α: Type u_1
α : Type _: Type (?u.175+1)
Type _) [Bornology: Type ?u.178 → Type ?u.178
Bornology α: Type ?u.175
α] : cobounded: (α : Type ?u.182) → [inst : Bornology α] → Filter α
cobounded α: Type ?u.175
α ≤ cofinite: {α : Type ?u.187} → Filter α
cofinite :=
Bornology.le_cofinite': ∀ {α : Type ?u.254} [self : Bornology α], cobounded' ≤ cofinite
Bornology.le_cofinite'
#align bornology.le_cofinite Bornology.le_cofinite: ∀ (α : Type u_1) [inst : Bornology α], Bornology.cobounded α ≤ cofinite
Bornology.le_cofinite

initialize_simps_projections Bornology: Type u_1 → Type u_1
Bornology (cobounded': (α : Type u_1) → Bornology α → Filter α
cobounded' → cobounded: (α : Type u_1) → [inst : Bornology α] → Filter α
cobounded)

@[ext]
lemma Bornology.ext: ∀ (t t' : Bornology α), cobounded α = cobounded α → t = t'
Bornology.ext (t: Bornology α
t t': Bornology α
t' : Bornology: Type ?u.301 → Type ?u.301
Bornology α: Type ?u.292
α)
    (h_cobounded: cobounded α = cobounded α
h_cobounded : @Bornology.cobounded: (α : Type ?u.305) → [inst : Bornology α] → Filter α
Bornology.cobounded α: Type ?u.292
α t: Bornology α
t = @Bornology.cobounded: (α : Type ?u.307) → [inst : Bornology α] → Filter α
Bornology.cobounded α: Type ?u.292
α t': Bornology α
t') :
    t: Bornology α
t = t': Bornology α
t' := by
Goals accomplished! 🐙
  ι: Type ?u.289

α: Type u_1

β: Type ?u.295

t, t': Bornology α

h_cobounded: cobounded α = cobounded α

t = t'cases t: Bornology α
tι: Type ?u.289

α: Type u_1

β: Type ?u.295

t': Bornology α

cobounded'✝: Filter α

le_cofinite'✝: cobounded'✝ ≤ cofinite

h_cobounded: cobounded α = cobounded α

mk{ cobounded' := cobounded'✝, le_cofinite' := le_cofinite'✝ } = t'
  ι: Type ?u.289

α: Type u_1

β: Type ?u.295

t, t': Bornology α

h_cobounded: cobounded α = cobounded α

t = t'cases t': Bornology α
t'ι: Type ?u.289

α: Type u_1

β: Type ?u.295

cobounded'✝¹: Filter α

le_cofinite'✝¹: cobounded'✝¹ ≤ cofinite

cobounded'✝: Filter α

le_cofinite'✝: cobounded'✝ ≤ cofinite

h_cobounded: cobounded α = cobounded α

mk.mk{ cobounded' := cobounded'✝¹, le_cofinite' := le_cofinite'✝¹ } =   { cobounded' := cobounded'✝, le_cofinite' := le_cofinite'✝ }
  ι: Type ?u.289

α: Type u_1

β: Type ?u.295

t, t': Bornology α

h_cobounded: cobounded α = cobounded α

t = t'congr
Goals accomplished! 🐙
#align bornology.ext Bornology.ext: ∀ {α : Type u_1} (t t' : Bornology α), Bornology.cobounded α = Bornology.cobounded α → t = t'
Bornology.ext

lemma Bornology.ext_iff: ∀ {α : Type u_1} (t t' : Bornology α), t = t' ↔ cobounded α = cobounded α
Bornology.ext_iff (t: Bornology α
t t': Bornology α
t' : Bornology: Type ?u.612 → Type ?u.612
Bornology α: Type ?u.603
α) :
    t: Bornology α
t = t': Bornology α
t' ↔ @Bornology.cobounded: (α : Type ?u.619) → [inst : Bornology α] → Filter α
Bornology.cobounded α: Type ?u.603
α t: Bornology α
t = @Bornology.cobounded: (α : Type ?u.620) → [inst : Bornology α] → Filter α
Bornology.cobounded α: Type ?u.603
α t': Bornology α
t' :=
⟨congrArg: ∀ {α : Sort ?u.635} {β : Sort ?u.634} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congrArg _: ?m.636 → ?m.637
_, Bornology.ext: ∀ {α : Type ?u.648} (t t' : Bornology α), cobounded α = cobounded α → t = t'
Bornology.ext _: Bornology ?m.649
_ _: Bornology ?m.649
_⟩
#align bornology.ext_iff Bornology.ext_iff: ∀ {α : Type u_1} (t t' : Bornology α), t = t' ↔ Bornology.cobounded α = Bornology.cobounded α
Bornology.ext_iff

/-- A constructor for bornologies by specifying the bounded sets,
and showing that they satisfy the appropriate conditions. -/
@[simps: ∀ {α : Type u_1} (B : Set (Set α)) (empty_mem : ∅ ∈ B)
  (subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B)
  (union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B) (singleton_mem : ∀ (x : α), {x} ∈ B),
  (cobounded α).sets = { s | sᶜ ∈ B }
simps]
def Bornology.ofBounded: {α : Type u_1} →
  (B : Set (Set α)) →
    ∅ ∈ B →
      (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B) →
        (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B) → (∀ (x : α), {x} ∈ B) → Bornology α
Bornology.ofBounded {α: Type ?u.672
α : Type _: Type (?u.672+1)
Type _} (B: Set (Set α)
B : Set: Type ?u.675 → Type ?u.675
Set (Set: Type ?u.676 → Type ?u.676
Set α: Type ?u.672
α))
    (empty_mem: ∅ ∈ B
empty_mem : ∅: ?m.701
∅ ∈ B: Set (Set α)
B)
    (subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
subset_mem : ∀ s₁: ?m.792
s₁ (_: s₁ ∈ B
_ : s₁: ?m.792
s₁ ∈ B: Set (Set α)
B) s₂: ?m.827
s₂, s₂: ?m.827
s₂ ⊆ s₁: ?m.792
s₁ → s₂: ?m.827
s₂ ∈ B: Set (Set α)
B)
    (union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
union_mem : ∀ s₁: ?m.884
s₁ (_: s₁ ∈ B
_ : s₁: ?m.884
s₁ ∈ B: Set (Set α)
B) s₂: ?m.919
s₂ (_: s₂ ∈ B
_ : s₂: ?m.919
s₂ ∈ B: Set (Set α)
B), s₁: ?m.884
s₁ ∪ s₂: ?m.919
s₂ ∈ B: Set (Set α)
B)
    (singleton_mem: ∀ (x : ?m.1001), ?m.1064 x ∈ B
singleton_mem : ∀ x: ?m.1001
x, {x: ?m.1001
x} ∈ B: Set (Set α)
B) : Bornology: Type ?u.1068 → Type ?u.1068
Bornology α: Type ?u.672
α
    where
  cobounded' :=
    { sets := { s: Set α
s : Set: Type ?u.1127 → Type ?u.1127
Set α: Type ?u.672
α | s: Set α
sᶜ ∈ B: Set (Set α)
B }
      univ_sets := by
Goals accomplished! 🐙 ι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

univ ∈ { s | sᶜ ∈ B }rwa [ι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

univ ∈ { s | sᶜ ∈ B }← compl_univ: ∀ {α : Type ?u.1278}, univᶜ = ∅
compl_univι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: univᶜ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

univ ∈ { s | sᶜ ∈ B }]ι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: univᶜ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

univ ∈ { s | sᶜ ∈ B } at empty_mem: ∅ ∈ B
empty_mem
Goals accomplished! 🐙
      sets_of_superset := fun hx: ?m.1175
hx hy: ?m.1178
hy => subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
subset_mem _: Set α
_ hx: ?m.1175
hx _: Set α
_ (compl_subset_compl: ∀ {α : Type ?u.1207} {s t : Set α}, sᶜ ⊆ tᶜ ↔ t ⊆ s
compl_subset_compl.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr hy: ?m.1178
hy)
      inter_sets := fun hx: ?m.1252
hx hy: ?m.1255
hy => by
Goals accomplished! 🐙 ι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

x✝, y✝: Set α

hx: x✝ ∈ { s | sᶜ ∈ B }

hy: y✝ ∈ { s | sᶜ ∈ B }

x✝ ∩ y✝ ∈ { s | sᶜ ∈ B }simpa [compl_inter: ∀ {α : Type ?u.1321} (s t : Set α), (s ∩ t)ᶜ = sᶜ ∪ tᶜ
compl_inter] using union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
union_mem _: Set α
_ hx: x✝ ∈ { s | sᶜ ∈ B }
hx _: Set α
_ hy: y✝ ∈ { s | sᶜ ∈ B }
hy
Goals accomplished! 🐙 }
  le_cofinite' := by
Goals accomplished! 🐙
    ι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

{ sets := { s | sᶜ ∈ B }, univ_sets := (_ : univᶜ ∈ B),
    sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → x ⊆ y → yᶜ ∈ B),
    inter_sets := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → y ∈ { s | sᶜ ∈ B } → x ∩ y ∈ { s | sᶜ ∈ B }) } ≤   cofiniterw [ι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

{ sets := { s | sᶜ ∈ B }, univ_sets := (_ : univᶜ ∈ B),
    sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → x ⊆ y → yᶜ ∈ B),
    inter_sets := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → y ∈ { s | sᶜ ∈ B } → x ∩ y ∈ { s | sᶜ ∈ B }) } ≤   cofinitele_cofinite_iff_compl_singleton_mem: ∀ {α : Type ?u.1893} {l : Filter α}, l ≤ cofinite ↔ ∀ (x : α), {x}ᶜ ∈ l
le_cofinite_iff_compl_singleton_memι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

∀ (x : α),
  {x}ᶜ ∈     { sets := { s | sᶜ ∈ B }, univ_sets := (_ : univᶜ ∈ B),
      sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → x ⊆ y → yᶜ ∈ B),
      inter_sets := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → y ∈ { s | sᶜ ∈ B } → x ∩ y ∈ { s | sᶜ ∈ B }) }]ι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

∀ (x : α),
  {x}ᶜ ∈     { sets := { s | sᶜ ∈ B }, univ_sets := (_ : univᶜ ∈ B),
      sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → x ⊆ y → yᶜ ∈ B),
      inter_sets := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → y ∈ { s | sᶜ ∈ B } → x ∩ y ∈ { s | sᶜ ∈ B }) }
    ι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

{ sets := { s | sᶜ ∈ B }, univ_sets := (_ : univᶜ ∈ B),
    sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → x ⊆ y → yᶜ ∈ B),
    inter_sets := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → y ∈ { s | sᶜ ∈ B } → x ∩ y ∈ { s | sᶜ ∈ B }) } ≤   cofiniteintro x: α
xι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

x: α

{x}ᶜ ∈   { sets := { s | sᶜ ∈ B }, univ_sets := (_ : univᶜ ∈ B),
    sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → x ⊆ y → yᶜ ∈ B),
    inter_sets := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → y ∈ { s | sᶜ ∈ B } → x ∩ y ∈ { s | sᶜ ∈ B }) }
    ι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

{ sets := { s | sᶜ ∈ B }, univ_sets := (_ : univᶜ ∈ B),
    sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → x ⊆ y → yᶜ ∈ B),
    inter_sets := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → y ∈ { s | sᶜ ∈ B } → x ∩ y ∈ { s | sᶜ ∈ B }) } ≤   cofinitechange {x: α
x}ᶜᶜ ∈ B: Set (Set α)
Bι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

x: α

{x}ᶜᶜ ∈ B
    ι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

{ sets := { s | sᶜ ∈ B }, univ_sets := (_ : univᶜ ∈ B),
    sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → x ⊆ y → yᶜ ∈ B),
    inter_sets := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → y ∈ { s | sᶜ ∈ B } → x ∩ y ∈ { s | sᶜ ∈ B }) } ≤   cofiniterw [ι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

x: α

{x}ᶜᶜ ∈ Bcompl_compl: ∀ {α : Type ?u.2208} [inst : BooleanAlgebra α] (x : α), xᶜᶜ = x
compl_complι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

x: α

{x} ∈ B]ι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

x: α

{x} ∈ B
    ι: Type ?u.663

α✝: Type ?u.666

β: Type ?u.669

α: Type ?u.672

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

singleton_mem: ∀ (x : α), {x} ∈ B

{ sets := { s | sᶜ ∈ B }, univ_sets := (_ : univᶜ ∈ B),
    sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → x ⊆ y → yᶜ ∈ B),
    inter_sets := (_ : ∀ {x y : Set α}, x ∈ { s | sᶜ ∈ B } → y ∈ { s | sᶜ ∈ B } → x ∩ y ∈ { s | sᶜ ∈ B }) } ≤   cofiniteexact singleton_mem: ∀ (x : α), {x} ∈ B
singleton_mem x: α
x
Goals accomplished! 🐙
#align bornology.of_bounded Bornology.ofBounded: {α : Type u_1} →
  (B : Set (Set α)) →
    ∅ ∈ B →
      (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B) →
        (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B) → (∀ (x : α), {x} ∈ B) → Bornology α
Bornology.ofBounded
#align bornology.of_bounded_cobounded_sets Bornology.ofBounded_cobounded_sets: ∀ {α : Type u_1} (B : Set (Set α)) (empty_mem : ∅ ∈ B)
  (subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B)
  (union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B) (singleton_mem : ∀ (x : α), {x} ∈ B),
  (Bornology.cobounded α).sets = { s | sᶜ ∈ B }
Bornology.ofBounded_cobounded_sets

/-- A constructor for bornologies by specifying the bounded sets,
and showing that they satisfy the appropriate conditions. -/
@[simps!]
def Bornology.ofBounded': {α : Type u_1} →
  (B : Set (Set α)) →
    ∅ ∈ B →
      (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B) →
        (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B) → ⋃₀ B = univ → Bornology α
Bornology.ofBounded' {α: Type ?u.2567
α : Type _: Type (?u.2567+1)
Type _} (B: Set (Set α)
B : Set: Type ?u.2570 → Type ?u.2570
Set (Set: Type ?u.2571 → Type ?u.2571
Set α: Type ?u.2567
α))
    (empty_mem: ∅ ∈ B
empty_mem : ∅: ?m.2596
∅ ∈ B: Set (Set α)
B)
    (subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
subset_mem : ∀ s₁: ?m.2687
s₁ (_: s₁ ∈ B
_ : s₁: ?m.2687
s₁ ∈ B: Set (Set α)
B) s₂: ?m.2722
s₂, s₂: ?m.2722
s₂ ⊆ s₁: ?m.2687
s₁ → s₂: ?m.2722
s₂ ∈ B: Set (Set α)
B)
    (union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
union_mem : ∀ s₁: ?m.2779
s₁ (_: s₁ ∈ B
_ : s₁: ?m.2779
s₁ ∈ B: Set (Set α)
B) s₂: ?m.2814
s₂ (_: s₂ ∈ B
_ : s₂: ?m.2814
s₂ ∈ B: Set (Set α)
B), s₁: ?m.2779
s₁ ∪ s₂: ?m.2814
s₂ ∈ B: Set (Set α)
B)
    (sUnion_univ: ⋃₀ B = univ
sUnion_univ : ⋃₀ B: Set (Set α)
B = univ: {α : Type ?u.2901} → Set α
univ) :
    Bornology: Type ?u.2934 → Type ?u.2934
Bornology α: Type ?u.2567
α :=
  Bornology.ofBounded: {α : Type ?u.2955} →
  (B : Set (Set α)) →
    ∅ ∈ B →
      (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B) →
        (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B) → (∀ (x : α), {x} ∈ B) → Bornology α
Bornology.ofBounded B: Set (Set α)
B empty_mem: ∅ ∈ B
empty_mem subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
subset_mem union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
union_mem fun x: ?m.2984
x => by
Goals accomplished! 🐙
    ι: Type ?u.2558

α✝: Type ?u.2561

β: Type ?u.2564

α: Type ?u.2567

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ⋃₀ B = univ

x: α

{x} ∈ Brw [ι: Type ?u.2558

α✝: Type ?u.2561

β: Type ?u.2564

α: Type ?u.2567

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ⋃₀ B = univ

x: α

{x} ∈ BsUnion_eq_univ_iff: ∀ {α : Type ?u.2991} {c : Set (Set α)}, ⋃₀ c = univ ↔ ∀ (a : α), ∃ b, b ∈ c ∧ a ∈ b
sUnion_eq_univ_iffι: Type ?u.2558

α✝: Type ?u.2561

β: Type ?u.2564

α: Type ?u.2567

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (a : α), ∃ b, b ∈ B ∧ a ∈ b

x: α

{x} ∈ B]ι: Type ?u.2558

α✝: Type ?u.2561

β: Type ?u.2564

α: Type ?u.2567

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (a : α), ∃ b, b ∈ B ∧ a ∈ b

x: α

{x} ∈ B at sUnion_univ: ⋃₀ B = univ
sUnion_univι: Type ?u.2558

α✝: Type ?u.2561

β: Type ?u.2564

α: Type ?u.2567

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (a : α), ∃ b, b ∈ B ∧ a ∈ b

x: α

{x} ∈ B
    ι: Type ?u.2558

α✝: Type ?u.2561

β: Type ?u.2564

α: Type ?u.2567

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ⋃₀ B = univ

x: α

{x} ∈ Brcases sUnion_univ: ∀ (a : α), ∃ b, b ∈ B ∧ a ∈ b
sUnion_univ x: α
x with ⟨s, hs, hxs⟩: s ∈ B ∧ x ∈ s
⟨s: Set α
s⟨s, hs, hxs⟩: s ∈ B ∧ x ∈ s
, hs: s ∈ B
hs⟨s, hs, hxs⟩: s ∈ B ∧ x ∈ s
, hxs: x ∈ s
hxs⟨s, hs, hxs⟩: s ∈ B ∧ x ∈ s
⟩ι: Type ?u.2558

α✝: Type ?u.2561

β: Type ?u.2564

α: Type ?u.2567

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (a : α), ∃ b, b ∈ B ∧ a ∈ b

x: α

s: Set α

hs: s ∈ B

hxs: x ∈ s

intro.intro{x} ∈ B
    ι: Type ?u.2558

α✝: Type ?u.2561

β: Type ?u.2564

α: Type ?u.2567

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ⋃₀ B = univ

x: α

{x} ∈ Bexact subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
subset_mem s: Set α
s hs: s ∈ B
hs {x: α
x} (singleton_subset_iff: ∀ {α : Type ?u.3100} {a : α} {s : Set α}, {a} ⊆ s ↔ a ∈ s
singleton_subset_iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr hxs: x ∈ s
hxs)
Goals accomplished! 🐙
#align bornology.of_bounded' Bornology.ofBounded': {α : Type u_1} →
  (B : Set (Set α)) →
    ∅ ∈ B →
      (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B) →
        (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B) → ⋃₀ B = univ → Bornology α
Bornology.ofBounded'
#align bornology.of_bounded'_cobounded_sets Bornology.ofBounded'_cobounded_sets: ∀ {α : Type u_1} (B : Set (Set α)) (empty_mem : ∅ ∈ B)
  (subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B)
  (union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B) (sUnion_univ : ⋃₀ B = univ),
  (Bornology.cobounded α).sets = { s | sᶜ ∈ B }
Bornology.ofBounded'_cobounded_sets
namespace Bornology

section

variable [Bornology: Type ?u.3908 → Type ?u.3908
Bornology α: Type ?u.3902
α] {s: Set α
s t: Set α
t : Set: Type ?u.3782 → Type ?u.3782
Set α: Type ?u.3700
α} {x: α
x : α: Type ?u.3700
α}

/-- `IsCobounded` is the predicate that `s` is in the filter of cobounded sets in the ambient
bornology on `α` -/
def IsCobounded: {α : Type u_1} → [inst : Bornology α] → Set α → Prop
IsCobounded (s: Set α
s : Set: Type ?u.3737 → Type ?u.3737
Set α: Type ?u.3720
α) : Prop: Type
Prop :=
  s: Set α
s ∈ cobounded: (α : Type ?u.3748) → [inst : Bornology α] → Filter α
cobounded α: Type ?u.3720
α
#align bornology.is_cobounded Bornology.IsCobounded: {α : Type u_1} → [inst : Bornology α] → Set α → Prop
Bornology.IsCobounded

/-- `IsBounded` is the predicate that `s` is bounded relative to the ambient bornology on `α`. -/
def IsBounded: Set α → Prop
IsBounded (s: Set α
s : Set: Type ?u.3790 → Type ?u.3790
Set α: Type ?u.3773
α) : Prop: Type
Prop :=
  IsCobounded: {α : Type ?u.3795} → [inst : Bornology α] → Set α → Prop
IsCobounded (s: Set α
sᶜ)
#align bornology.is_bounded Bornology.IsBounded: {α : Type u_1} → [inst : Bornology α] → Set α → Prop
Bornology.IsBounded

theorem isCobounded_def: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsCobounded s ↔ s ∈ cobounded α
isCobounded_def {s: Set α
s : Set: Type ?u.3860 → Type ?u.3860
Set α: Type ?u.3843
α} : IsCobounded: {α : Type ?u.3863} → [inst : Bornology α] → Set α → Prop
IsCobounded s: Set α
s ↔ s: Set α
s ∈ cobounded: (α : Type ?u.3878) → [inst : Bornology α] → Filter α
cobounded α: Type ?u.3843
α :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align bornology.is_cobounded_def Bornology.isCobounded_def: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsCobounded s ↔ s ∈ cobounded α
Bornology.isCobounded_def

theorem isBounded_def: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsBounded s ↔ sᶜ ∈ cobounded α
isBounded_def {s: Set α
s : Set: Type ?u.3919 → Type ?u.3919
Set α: Type ?u.3902
α} : IsBounded: {α : Type ?u.3922} → [inst : Bornology α] → Set α → Prop
IsBounded s: Set α
s ↔ s: Set α
sᶜ ∈ cobounded: (α : Type ?u.3966) → [inst : Bornology α] → Filter α
cobounded α: Type ?u.3902
α :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align bornology.is_bounded_def Bornology.isBounded_def: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsBounded s ↔ sᶜ ∈ cobounded α
Bornology.isBounded_def

@[simp]
theorem isBounded_compl_iff: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsBounded (sᶜ) ↔ IsCobounded s
isBounded_compl_iff : IsBounded: {α : Type ?u.4007} → [inst : Bornology α] → Set α → Prop
IsBounded (s: Set α
sᶜ) ↔ IsCobounded: {α : Type ?u.4045} → [inst : Bornology α] → Set α → Prop
IsCobounded s: Set α
s := by
Goals accomplished! 🐙
  ι: Type ?u.3987

α: Type u_1

β: Type ?u.3993

inst✝: Bornology α

s, t: Set α

x: α

IsBounded (sᶜ) ↔ IsCobounded srw [ι: Type ?u.3987

α: Type u_1

β: Type ?u.3993

inst✝: Bornology α

s, t: Set α

x: α

IsBounded (sᶜ) ↔ IsCobounded sisBounded_def: ∀ {α : Type ?u.4052} [inst : Bornology α] {s : Set α}, IsBounded s ↔ sᶜ ∈ cobounded α
isBounded_def,ι: Type ?u.3987

α: Type u_1

β: Type ?u.3993

inst✝: Bornology α

s, t: Set α

x: α

sᶜᶜ ∈ cobounded α ↔ IsCobounded s ι: Type ?u.3987

α: Type u_1

β: Type ?u.3993

inst✝: Bornology α

s, t: Set α

x: α

IsBounded (sᶜ) ↔ IsCobounded sisCobounded_def: ∀ {α : Type ?u.4069} [inst : Bornology α] {s : Set α}, IsCobounded s ↔ s ∈ cobounded α
isCobounded_def,ι: Type ?u.3987

α: Type u_1

β: Type ?u.3993

inst✝: Bornology α

s, t: Set α

x: α

sᶜᶜ ∈ cobounded α ↔ s ∈ cobounded α ι: Type ?u.3987

α: Type u_1

β: Type ?u.3993

inst✝: Bornology α

s, t: Set α

x: α

IsBounded (sᶜ) ↔ IsCobounded scompl_compl: ∀ {α : Type ?u.4083} [inst : BooleanAlgebra α] (x : α), xᶜᶜ = x
compl_complι: Type ?u.3987

α: Type u_1

β: Type ?u.3993

inst✝: Bornology α

s, t: Set α

x: α

s ∈ cobounded α ↔ s ∈ cobounded α]
Goals accomplished! 🐙
#align bornology.is_bounded_compl_iff Bornology.isBounded_compl_iff: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsBounded (sᶜ) ↔ IsCobounded s
Bornology.isBounded_compl_iff

@[simp]
theorem isCobounded_compl_iff: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsCobounded (sᶜ) ↔ IsBounded s
isCobounded_compl_iff : IsCobounded: {α : Type ?u.4175} → [inst : Bornology α] → Set α → Prop
IsCobounded (s: Set α
sᶜ) ↔ IsBounded: {α : Type ?u.4213} → [inst : Bornology α] → Set α → Prop
IsBounded s: Set α
s :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align bornology.is_cobounded_compl_iff Bornology.isCobounded_compl_iff: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsCobounded (sᶜ) ↔ IsBounded s
Bornology.isCobounded_compl_iff

alias isBounded_compl_iff: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsBounded (sᶜ) ↔ IsCobounded s
isBounded_compl_iff ↔ IsBounded.of_compl: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsBounded (sᶜ) → IsCobounded s
IsBounded.of_compl IsCobounded.compl: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsCobounded s → IsBounded (sᶜ)
IsCobounded.compl
#align bornology.is_bounded.of_compl Bornology.IsBounded.of_compl: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsBounded (sᶜ) → IsCobounded s
Bornology.IsBounded.of_compl
#align bornology.is_cobounded.compl Bornology.IsCobounded.compl: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsCobounded s → IsBounded (sᶜ)
Bornology.IsCobounded.compl

alias isCobounded_compl_iff: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsCobounded (sᶜ) ↔ IsBounded s
isCobounded_compl_iff ↔ IsCobounded.of_compl: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsCobounded (sᶜ) → IsBounded s
IsCobounded.of_compl IsBounded.compl: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsBounded s → IsCobounded (sᶜ)
IsBounded.compl
#align bornology.is_cobounded.of_compl Bornology.IsCobounded.of_compl: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsCobounded (sᶜ) → IsBounded s
Bornology.IsCobounded.of_compl
#align bornology.is_bounded.compl Bornology.IsBounded.compl: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsBounded s → IsCobounded (sᶜ)
Bornology.IsBounded.compl

@[simp]
theorem isBounded_empty: IsBounded ∅
isBounded_empty : IsBounded: {α : Type ?u.4291} → [inst : Bornology α] → Set α → Prop
IsBounded (∅: ?m.4299
∅ : Set: Type ?u.4297 → Type ?u.4297
Set α: Type ?u.4274
α) := by
Goals accomplished! 🐙
  ι: Type ?u.4271

α: Type u_1

β: Type ?u.4277

inst✝: Bornology α

s, t: Set α

x: α

IsBounded ∅rw [ι: Type ?u.4271

α: Type u_1

β: Type ?u.4277

inst✝: Bornology α

s, t: Set α

x: α

IsBounded ∅isBounded_def: ∀ {α : Type ?u.4350} [inst : Bornology α] {s : Set α}, IsBounded s ↔ sᶜ ∈ cobounded α
isBounded_def,ι: Type ?u.4271

α: Type u_1

β: Type ?u.4277

inst✝: Bornology α

s, t: Set α

x: α

∅ᶜ ∈ cobounded α ι: Type ?u.4271

α: Type u_1

β: Type ?u.4277

inst✝: Bornology α

s, t: Set α

x: α

IsBounded ∅compl_empty: ∀ {α : Type ?u.4367}, ∅ᶜ = univ
compl_emptyι: Type ?u.4271

α: Type u_1

β: Type ?u.4277

inst✝: Bornology α

s, t: Set α

x: α

univ ∈ cobounded α]ι: Type ?u.4271

α: Type u_1

β: Type ?u.4277

inst✝: Bornology α

s, t: Set α

x: α

univ ∈ cobounded α
  ι: Type ?u.4271

α: Type u_1

β: Type ?u.4277

inst✝: Bornology α

s, t: Set α

x: α

IsBounded ∅exact univ_mem: ∀ {α : Type ?u.4385} {f : Filter α}, univ ∈ f
univ_mem
Goals accomplished! 🐙
#align bornology.is_bounded_empty Bornology.isBounded_empty: ∀ {α : Type u_1} [inst : Bornology α], IsBounded ∅
Bornology.isBounded_empty

@[simp]
theorem isBounded_singleton: ∀ {α : Type u_1} [inst : Bornology α] {x : α}, IsBounded {x}
isBounded_singleton : IsBounded: {α : Type ?u.4435} → [inst : Bornology α] → Set α → Prop
IsBounded ({x: α
x} : Set: Type ?u.4441 → Type ?u.4441
Set α: Type ?u.4418
α) := by
Goals accomplished! 🐙
  ι: Type ?u.4415

α: Type u_1

β: Type ?u.4421

inst✝: Bornology α

s, t: Set α

x: α

IsBounded {x}rw [ι: Type ?u.4415

α: Type u_1

β: Type ?u.4421

inst✝: Bornology α

s, t: Set α

x: α

IsBounded {x}isBounded_def: ∀ {α : Type ?u.4473} [inst : Bornology α] {s : Set α}, IsBounded s ↔ sᶜ ∈ cobounded α
isBounded_defι: Type ?u.4415

α: Type u_1

β: Type ?u.4421

inst✝: Bornology α

s, t: Set α

x: α

{x}ᶜ ∈ cobounded α]ι: Type ?u.4415

α: Type u_1

β: Type ?u.4421

inst✝: Bornology α

s, t: Set α

x: α

{x}ᶜ ∈ cobounded α
  ι: Type ?u.4415

α: Type u_1

β: Type ?u.4421

inst✝: Bornology α

s, t: Set α

x: α

IsBounded {x}exact le_cofinite: ∀ (α : Type ?u.4494) [inst : Bornology α], cobounded α ≤ cofinite
le_cofinite _: Type ?u.4494
_ (finite_singleton: ∀ {α : Type ?u.4510} (a : α), Set.Finite {a}
finite_singleton x: α
x).compl_mem_cofinite: ∀ {α : Type ?u.4512} {s : Set α}, Set.Finite s → sᶜ ∈ cofinite
compl_mem_cofinite
Goals accomplished! 🐙
#align bornology.is_bounded_singleton Bornology.isBounded_singleton: ∀ {α : Type u_1} [inst : Bornology α] {x : α}, IsBounded {x}
Bornology.isBounded_singleton

@[simp]
theorem isCobounded_univ: ∀ {α : Type u_1} [inst : Bornology α], IsCobounded univ
isCobounded_univ : IsCobounded: {α : Type ?u.4565} → [inst : Bornology α] → Set α → Prop
IsCobounded (univ: {α : Type ?u.4572} → Set α
univ : Set: Type ?u.4571 → Type ?u.4571
Set α: Type ?u.4548
α) :=
  univ_mem: ∀ {α : Type ?u.4580} {f : Filter α}, univ ∈ f
univ_mem
#align bornology.is_cobounded_univ Bornology.isCobounded_univ: ∀ {α : Type u_1} [inst : Bornology α], IsCobounded univ
Bornology.isCobounded_univ

@[simp]
theorem isCobounded_inter: ∀ {α : Type u_1} [inst : Bornology α] {s t : Set α}, IsCobounded (s ∩ t) ↔ IsCobounded s ∧ IsCobounded t
isCobounded_inter : IsCobounded: {α : Type ?u.4627} → [inst : Bornology α] → Set α → Prop
IsCobounded (s: Set α
s ∩ t: Set α
t) ↔ IsCobounded: {α : Type ?u.4654} → [inst : Bornology α] → Set α → Prop
IsCobounded s: Set α
s ∧ IsCobounded: {α : Type ?u.4659} → [inst : Bornology α] → Set α → Prop
IsCobounded t: Set α
t :=
  inter_mem_iff: ∀ {α : Type ?u.4665} {f : Filter α} {s t : Set α}, s ∩ t ∈ f ↔ s ∈ f ∧ t ∈ f
inter_mem_iff
#align bornology.is_cobounded_inter Bornology.isCobounded_inter: ∀ {α : Type u_1} [inst : Bornology α] {s t : Set α}, IsCobounded (s ∩ t) ↔ IsCobounded s ∧ IsCobounded t
Bornology.isCobounded_inter

theorem IsCobounded.inter: IsCobounded s → IsCobounded t → IsCobounded (s ∩ t)
IsCobounded.inter (hs: IsCobounded s
hs : IsCobounded: {α : Type ?u.4738} → [inst : Bornology α] → Set α → Prop
IsCobounded s: Set α
s) (ht: IsCobounded t
ht : IsCobounded: {α : Type ?u.4751} → [inst : Bornology α] → Set α → Prop
IsCobounded t: Set α
t) : IsCobounded: {α : Type ?u.4760} → [inst : Bornology α] → Set α → Prop
IsCobounded (s: Set α
s ∩ t: Set α
t) :=
  isCobounded_inter: ∀ {α : Type ?u.4790} [inst : Bornology α] {s t : Set α}, IsCobounded (s ∩ t) ↔ IsCobounded s ∧ IsCobounded t
isCobounded_inter.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 ⟨hs: IsCobounded s
hs, ht: IsCobounded t
ht⟩
#align bornology.is_cobounded.inter Bornology.IsCobounded.inter: ∀ {α : Type u_1} [inst : Bornology α] {s t : Set α}, IsCobounded s → IsCobounded t → IsCobounded (s ∩ t)
Bornology.IsCobounded.inter

@[simp]
theorem isBounded_union: ∀ {α : Type u_1} [inst : Bornology α] {s t : Set α}, IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t
isBounded_union : IsBounded: {α : Type ?u.4848} → [inst : Bornology α] → Set α → Prop
IsBounded (s: Set α
s ∪ t: Set α
t) ↔ IsBounded: {α : Type ?u.4875} → [inst : Bornology α] → Set α → Prop
IsBounded s: Set α
s ∧ IsBounded: {α : Type ?u.4880} → [inst : Bornology α] → Set α → Prop
IsBounded t: Set α
t := by
Goals accomplished! 🐙
  ι: Type ?u.4828

α: Type u_1

β: Type ?u.4834

inst✝: Bornology α

s, t: Set α

x: α

IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded tsimp only [← isCobounded_compl_iff: ∀ {α : Type ?u.4898} [inst : Bornology α] {s : Set α}, IsCobounded (sᶜ) ↔ IsBounded s
isCobounded_compl_iff, compl_union: ∀ {α : Type ?u.4915} (s t : Set α), (s ∪ t)ᶜ = sᶜ ∩ tᶜ
compl_union, isCobounded_inter: ∀ {α : Type ?u.4931} [inst : Bornology α] {s t : Set α}, IsCobounded (s ∩ t) ↔ IsCobounded s ∧ IsCobounded t
isCobounded_inter]
Goals accomplished! 🐙
#align bornology.is_bounded_union Bornology.isBounded_union: ∀ {α : Type u_1} [inst : Bornology α] {s t : Set α}, IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t
Bornology.isBounded_union

theorem IsBounded.union: IsBounded s → IsBounded t → IsBounded (s ∪ t)
IsBounded.union (hs: IsBounded s
hs : IsBounded: {α : Type ?u.5132} → [inst : Bornology α] → Set α → Prop
IsBounded s: Set α
s) (ht: IsBounded t
ht : IsBounded: {α : Type ?u.5145} → [inst : Bornology α] → Set α → Prop
IsBounded t: Set α
t) : IsBounded: {α : Type ?u.5154} → [inst : Bornology α] → Set α → Prop
IsBounded (s: Set α
s ∪ t: Set α
t) :=
  isBounded_union: ∀ {α : Type ?u.5184} [inst : Bornology α] {s t : Set α}, IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t
isBounded_union.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 ⟨hs: IsBounded s
hs, ht: IsBounded t
ht⟩
#align bornology.is_bounded.union Bornology.IsBounded.union: ∀ {α : Type u_1} [inst : Bornology α] {s t : Set α}, IsBounded s → IsBounded t → IsBounded (s ∪ t)
Bornology.IsBounded.union

theorem IsCobounded.superset: ∀ {α : Type u_1} [inst : Bornology α] {s t : Set α}, IsCobounded s → s ⊆ t → IsCobounded t
IsCobounded.superset (hs: IsCobounded s
hs : IsCobounded: {α : Type ?u.5242} → [inst : Bornology α] → Set α → Prop
IsCobounded s: Set α
s) (ht: s ⊆ t
ht : s: Set α
s ⊆ t: Set α
t) : IsCobounded: {α : Type ?u.5275} → [inst : Bornology α] → Set α → Prop
IsCobounded t: Set α
t :=
  mem_of_superset: ∀ {α : Type ?u.5287} {f : Filter α} {x y : Set α}, x ∈ f → x ⊆ y → y ∈ f
mem_of_superset hs: IsCobounded s
hs ht: s ⊆ t
ht
#align bornology.is_cobounded.superset Bornology.IsCobounded.superset: ∀ {α : Type u_1} [inst : Bornology α] {s t : Set α}, IsCobounded s → s ⊆ t → IsCobounded t
Bornology.IsCobounded.superset

theorem IsBounded.subset: ∀ {α : Type u_1} [inst : Bornology α] {s t : Set α}, IsBounded t → s ⊆ t → IsBounded s
IsBounded.subset (ht: IsBounded t
ht : IsBounded: {α : Type ?u.5328} → [inst : Bornology α] → Set α → Prop
IsBounded t: Set α
t) (hs: s ⊆ t
hs : s: Set α
s ⊆ t: Set α
t) : IsBounded: {α : Type ?u.5361} → [inst : Bornology α] → Set α → Prop
IsBounded s: Set α
s :=
  ht: IsBounded t
ht.superset: ∀ {α : Type ?u.5373} [inst : Bornology α] {s t : Set α}, IsCobounded s → s ⊆ t → IsCobounded t
superset (compl_subset_compl: ∀ {α : Type ?u.5392} {s t : Set α}, sᶜ ⊆ tᶜ ↔ t ⊆ s
compl_subset_compl.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr hs: s ⊆ t
hs)
#align bornology.is_bounded.subset Bornology.IsBounded.subset: ∀ {α : Type u_1} [inst : Bornology α] {s t : Set α}, IsBounded t → s ⊆ t → IsBounded s
Bornology.IsBounded.subset

@[simp]
theorem sUnion_bounded_univ: ∀ {α : Type u_1} [inst : Bornology α], ⋃₀ { s | IsBounded s } = univ
sUnion_bounded_univ : ⋃₀ { s: Set α
s : Set: Type ?u.5449 → Type ?u.5449
Set α: Type ?u.5424
α | IsBounded: {α : Type ?u.5452} → [inst : Bornology α] → Set α → Prop
IsBounded s: Set α
s } = univ: {α : Type ?u.5464} → Set α
univ :=
  sUnion_eq_univ_iff: ∀ {α : Type ?u.5497} {c : Set (Set α)}, ⋃₀ c = univ ↔ ∀ (a : α), ∃ b, b ∈ c ∧ a ∈ b
sUnion_eq_univ_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 fun a: ?m.5514
a => ⟨{a: ?m.5514
a}, isBounded_singleton: ∀ {α : Type ?u.5561} [inst : Bornology α] {x : α}, IsBounded {x}
isBounded_singleton, mem_singleton: ∀ {α : Type ?u.5599} (a : α), a ∈ {a}
mem_singleton a: ?m.5514
a⟩
#align bornology.sUnion_bounded_univ Bornology.sUnion_bounded_univ: ∀ {α : Type u_1} [inst : Bornology α], ⋃₀ { s | IsBounded s } = univ
Bornology.sUnion_bounded_univ

theorem comap_cobounded_le_iff: ∀ [inst : Bornology β] {f : α → β},
  comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)
comap_cobounded_le_iff [Bornology: Type ?u.5644 → Type ?u.5644
Bornology β: Type ?u.5630
β] {f: α → β
f : α: Type ?u.5627
α → β: Type ?u.5630
β} :
    (cobounded: (α : Type ?u.5652) → [inst : Bornology α] → Filter α
cobounded β: Type ?u.5630
β).comap: {α : Type ?u.5658} → {β : Type ?u.5657} → (α → β) → Filter β → Filter α
comap f: α → β
f ≤ cobounded: (α : Type ?u.5669) → [inst : Bornology α] → Filter α
cobounded α: Type ?u.5627
α ↔ ∀ ⦃s: ?m.5709
s⦄, IsBounded: {α : Type ?u.5713} → [inst : Bornology α] → Set α → Prop
IsBounded s: ?m.5709
s → IsBounded: {α : Type ?u.5723} → [inst : Bornology α] → Set α → Prop
IsBounded (f: α → β
f '' s: ?m.5709
s) := by
Goals accomplished! 🐙
  ι: Type ?u.5624

α: Type u_2

β: Type u_1

inst✝¹: Bornology α

s, t: Set α

x: α

inst✝: Bornology β

f: α → β

comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)refine'
    ⟨fun h: ?m.5762
h s: ?m.5765
s hs: ?m.5768
hs => _: IsBounded (f '' s)
_, fun h: ?m.5777
h t: ?m.5782
t ht: ?m.5785
ht =>
      ⟨(f: α → β
f '' t: ?m.5782
tᶜ)ᶜ, h: ?m.5777
h <| IsCobounded.compl: ∀ {α : Type ?u.5892} [inst : Bornology α] {s : Set α}, IsCobounded s → IsBounded (sᶜ)
IsCobounded.compl ht: ?m.5785
ht, compl_subset_comm: ∀ {α : Type ?u.5908} {s t : Set α}, sᶜ ⊆ t ↔ tᶜ ⊆ s
compl_subset_comm.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 <| subset_preimage_image: ∀ {α : Type ?u.5931} {β : Type ?u.5932} (f : α → β) (s : Set α), s ⊆ f ⁻¹' (f '' s)
subset_preimage_image _: ?m.5933 → ?m.5934
_ _: Set ?m.5933
_⟩⟩ι: Type ?u.5624

α: Type u_2

β: Type u_1

inst✝¹: Bornology α

s✝, t: Set α

x: α

inst✝: Bornology β

f: α → β

h: comap f (cobounded β) ≤ cobounded α

s: Set α

hs: IsBounded s

IsBounded (f '' s)
  ι: Type ?u.5624

α: Type u_2

β: Type u_1

inst✝¹: Bornology α

s, t: Set α

x: α

inst✝: Bornology β

f: α → β

comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)obtain ⟨t, ht, hts⟩: t ∈ cobounded β ∧ f ⁻¹' t ⊆ sᶜ
⟨t: Set β
t⟨t, ht, hts⟩: t ∈ cobounded β ∧ f ⁻¹' t ⊆ sᶜ
, ht: t ∈ cobounded β
ht⟨t, ht, hts⟩: t ∈ cobounded β ∧ f ⁻¹' t ⊆ sᶜ
, hts: f ⁻¹' t ⊆ sᶜ
hts⟨t, ht, hts⟩: t ∈ cobounded β ∧ f ⁻¹' t ⊆ sᶜ
⟩ := h: ?m.5762
h hs: ?m.5768
hs.compl: ∀ {α : Type ?u.5980} [inst : Bornology α] {s : Set α}, IsBounded s → IsCobounded (sᶜ)
complι: Type ?u.5624

α: Type u_2

β: Type u_1

inst✝¹: Bornology α

s✝, t✝: Set α

x: α

inst✝: Bornology β

f: α → β

h: comap f (cobounded β) ≤ cobounded α

s: Set α

hs: IsBounded s

t: Set β

ht: t ∈ cobounded β

hts: f ⁻¹' t ⊆ sᶜ

intro.introIsBounded (f '' s)
  ι: Type ?u.5624

α: Type u_2

β: Type u_1

inst✝¹: Bornology α

s, t: Set α

x: α

inst✝: Bornology β

f: α → β

comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)rw [ι: Type ?u.5624

α: Type u_2

β: Type u_1

inst✝¹: Bornology α

s✝, t✝: Set α

x: α

inst✝: Bornology β

f: α → β

h: comap f (cobounded β) ≤ cobounded α

s: Set α

hs: IsBounded s

t: Set β

ht: t ∈ cobounded β

hts: f ⁻¹' t ⊆ sᶜ

intro.introIsBounded (f '' s)subset_compl_comm: ∀ {α : Type ?u.6043} {s t : Set α}, s ⊆ tᶜ ↔ t ⊆ sᶜ
subset_compl_comm,ι: Type ?u.5624

α: Type u_2

β: Type u_1

inst✝¹: Bornology α

s✝, t✝: Set α

x: α

inst✝: Bornology β

f: α → β

h: comap f (cobounded β) ≤ cobounded α

s: Set α

hs: IsBounded s

t: Set β

ht: t ∈ cobounded β

hts: s ⊆ (f ⁻¹' t)ᶜ

intro.introIsBounded (f '' s) ι: Type ?u.5624

α: Type u_2

β: Type u_1

inst✝¹: Bornology α

s✝, t✝: Set α

x: α

inst✝: Bornology β

f: α → β

h: comap f (cobounded β) ≤ cobounded α

s: Set α

hs: IsBounded s

t: Set β

ht: t ∈ cobounded β

hts: f ⁻¹' t ⊆ sᶜ

intro.introIsBounded (f '' s)← preimage_compl: ∀ {α : Type ?u.6069} {β : Type ?u.6068} {f : α → β} {s : Set β}, f ⁻¹' sᶜ = (f ⁻¹' s)ᶜ
preimage_complι: Type ?u.5624

α: Type u_2

β: Type u_1

inst✝¹: Bornology α

s✝, t✝: Set α

x: α

inst✝: Bornology β

f: α → β

h: comap f (cobounded β) ≤ cobounded α

s: Set α

hs: IsBounded s

t: Set β

ht: t ∈ cobounded β

hts: s ⊆ f ⁻¹' tᶜ

intro.introIsBounded (f '' s)]ι: Type ?u.5624

α: Type u_2

β: Type u_1

inst✝¹: Bornology α

s✝, t✝: Set α

x: α

inst✝: Bornology β

f: α → β

h: comap f (cobounded β) ≤ cobounded α

s: Set α

hs: IsBounded s

t: Set β

ht: t ∈ cobounded β

hts: s ⊆ f ⁻¹' tᶜ

intro.introIsBounded (f '' s) at hts: f ⁻¹' t ⊆ sᶜ
htsι: Type ?u.5624

α: Type u_2

β: Type u_1

inst✝¹: Bornology α

s✝, t✝: Set α

x: α

inst✝: Bornology β

f: α → β

h: comap f (cobounded β) ≤ cobounded α

s: Set α

hs: IsBounded s

t: Set β

ht: t ∈ cobounded β

hts: s ⊆ f ⁻¹' tᶜ

intro.introIsBounded (f '' s)
  ι: Type ?u.5624

α: Type u_2

β: Type u_1

inst✝¹: Bornology α

s, t: Set α

x: α

inst✝: Bornology β

f: α → β

comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)exact (IsCobounded.compl: ∀ {α : Type ?u.6101} [inst : Bornology α] {s : Set α}, IsCobounded s → IsBounded (sᶜ)
IsCobounded.compl ht: t ∈ cobounded β
ht).subset: ∀ {α : Type ?u.6117} [inst : Bornology α] {s t : Set α}, IsBounded t → s ⊆ t → IsBounded s
subset ((image_subset: ∀ {α : Type ?u.6132} {β : Type ?u.6133} {a b : Set α} (f : α → β), a ⊆ b → f '' a ⊆ f '' b
image_subset f: α → β
f hts: s ⊆ f ⁻¹' tᶜ
hts).trans: ∀ {α : Type ?u.6141} [inst : HasSubset α] [inst_1 : IsTrans α fun x x_1 => x ⊆ x_1] {a b c : α}, a ⊆ b → b ⊆ c → a ⊆ c
trans <| image_preimage_subset: ∀ {α : Type ?u.6191} {β : Type ?u.6190} (f : α → β) (s : Set β), f '' (f ⁻¹' s) ⊆ s
image_preimage_subset _: ?m.6192 → ?m.6193
_ _: Set ?m.6193
_)
Goals accomplished! 🐙
#align bornology.comap_cobounded_le_iff Bornology.comap_cobounded_le_iff: ∀ {α : Type u_2} {β : Type u_1} [inst : Bornology α] [inst_1 : Bornology β] {f : α → β},
  comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)
Bornology.comap_cobounded_le_iff

end

theorem ext_iff': ∀ {α : Type u_1} {t t' : Bornology α}, t = t' ↔ ∀ (s : Set α), sets (cobounded α) s ↔ sets (cobounded α) s
ext_iff' {t: Bornology α
t t': Bornology α
t' : Bornology: Type ?u.6242 → Type ?u.6242
Bornology α: Type ?u.6236
α} :
    t: Bornology α
t = t': Bornology α
t' ↔ ∀ s: ?m.6252
s, (@cobounded: (α : Type ?u.6255) → [inst : Bornology α] → Filter α
cobounded α: Type ?u.6236
α t: Bornology α
t).sets: {α : Type ?u.6256} → Filter α → Set (Set α)
sets s: ?m.6252
s ↔ (@cobounded: (α : Type ?u.6260) → [inst : Bornology α] → Filter α
cobounded α: Type ?u.6236
α t': Bornology α
t').sets: {α : Type ?u.6261} → Filter α → Set (Set α)
sets s: ?m.6252
s :=
  (Bornology.ext_iff: ∀ {α : Type ?u.6268} (t t' : Bornology α), t = t' ↔ cobounded α = cobounded α
Bornology.ext_iff _: Bornology ?m.6269
_ _: Bornology ?m.6269
_).trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans Filter.ext_iff: ∀ {α : Type ?u.6287} {f g : Filter α}, f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
Filter.ext_iff
#align bornology.ext_iff' Bornology.ext_iff': ∀ {α : Type u_1} {t t' : Bornology α}, t = t' ↔ ∀ (s : Set α), sets (cobounded α) s ↔ sets (cobounded α) s
Bornology.ext_iff'

theorem ext_iff_isBounded: ∀ {α : Type u_1} {t t' : Bornology α}, t = t' ↔ ∀ (s : Set α), IsBounded s ↔ IsBounded s
ext_iff_isBounded {t: Bornology α
t t': Bornology α
t' : Bornology: Type ?u.6312 → Type ?u.6312
Bornology α: Type ?u.6303
α} :
    t: Bornology α
t = t': Bornology α
t' ↔ ∀ s: ?m.6319
s, @IsBounded: {α : Type ?u.6322} → [inst : Bornology α] → Set α → Prop
IsBounded α: Type ?u.6303
α t: Bornology α
t s: ?m.6319
s ↔ @IsBounded: {α : Type ?u.6324} → [inst : Bornology α] → Set α → Prop
IsBounded α: Type ?u.6303
α t': Bornology α
t' s: ?m.6319
s :=
  ⟨fun h: ?m.6340
h s: ?m.6343
s => h: ?m.6340
h ▸ Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl, fun h: ?m.6356
h => by
Goals accomplished! 🐙
    ι: Type ?u.6300

α: Type u_1

β: Type ?u.6306

t, t': Bornology α

h: ∀ (s : Set α), IsBounded s ↔ IsBounded s

t = t'ext s: Set ?α
sι: Type ?u.6300

α: Type u_1

β: Type ?u.6306

t, t': Bornology α

h: ∀ (s : Set α), IsBounded s ↔ IsBounded s

s: Set α

h_cobounded.as ∈ cobounded α ↔ s ∈ cobounded α
    ι: Type ?u.6300

α: Type u_1

β: Type ?u.6306

t, t': Bornology α

h: ∀ (s : Set α), IsBounded s ↔ IsBounded s

t = t'simpa [@isBounded_def: ∀ {α : Type ?u.6408} [inst : Bornology α] {s : Set α}, IsBounded s ↔ sᶜ ∈ cobounded α
isBounded_def _: Type ?u.6408
_ t: Bornology α
t, isBounded_def: ∀ {α : Type ?u.6423} [inst : Bornology α] {s : Set α}, IsBounded s ↔ sᶜ ∈ cobounded α
isBounded_def, compl_compl: ∀ {α : Type ?u.6440} [inst : BooleanAlgebra α] (x : α), xᶜᶜ = x
compl_compl] using h: ∀ (s : Set α), IsBounded s ↔ IsBounded s
h (s: Set ?α
sᶜ)
Goals accomplished! 🐙⟩
-- porting note: Lean 3 could do this without `@isBounded_def _ t`
#align bornology.ext_iff_is_bounded Bornology.ext_iff_isBounded: ∀ {α : Type u_1} {t t' : Bornology α}, t = t' ↔ ∀ (s : Set α), IsBounded s ↔ IsBounded s
Bornology.ext_iff_isBounded

variable {s: Set α
s : Set: Type ?u.6790 → Type ?u.6790
Set α: Type ?u.6620
α}

theorem isCobounded_ofBounded_iff: ∀ (B : Set (Set α)) {empty_mem : ∅ ∈ B} {subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B}
  {union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B} {sUnion_univ : ∀ (x : α), {x} ∈ B},
  IsCobounded s ↔ sᶜ ∈ B
isCobounded_ofBounded_iff (B: Set (Set α)
B : Set: Type ?u.6641 → Type ?u.6641
Set (Set: Type ?u.6642 → Type ?u.6642
Set α: Type ?u.6632
α)) {empty_mem: ∅ ∈ B
empty_mem subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
subset_mem union_mem: ?m.6651
union_mem sUnion_univ: ∀ (x : α), {x} ∈ B
sUnion_univ} :
    @IsCobounded: {α : Type ?u.6657} → [inst : Bornology α] → Set α → Prop
IsCobounded _: Type ?u.6657
_ (ofBounded: {α : Type ?u.6659} →
  (B : Set (Set α)) →
    ∅ ∈ B →
      (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B) →
        (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B) → (∀ (x : α), {x} ∈ B) → Bornology α
ofBounded B: Set (Set α)
B empty_mem: ?m.6645
empty_mem subset_mem: ?m.6648
subset_mem union_mem: ?m.6651
union_mem sUnion_univ: ?m.6654
sUnion_univ) s: Set α
s ↔ s: Set α
sᶜ ∈ B: Set (Set α)
B :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align bornology.is_cobounded_of_bounded_iff Bornology.isCobounded_ofBounded_iff: ∀ {α : Type u_1} {s : Set α} (B : Set (Set α)) {empty_mem : ∅ ∈ B}
  {subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B}
  {union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B} {sUnion_univ : ∀ (x : α), {x} ∈ B},
  IsCobounded s ↔ sᶜ ∈ B
Bornology.isCobounded_ofBounded_iff

theorem isBounded_ofBounded_iff: ∀ (B : Set (Set α)) {empty_mem : ∅ ∈ B} {subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B}
  {union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B} {sUnion_univ : ∀ (x : α), {x} ∈ B},
  IsBounded s ↔ s ∈ B
isBounded_ofBounded_iff (B: Set (Set α)
B : Set: Type ?u.6793 → Type ?u.6793
Set (Set: Type ?u.6794 → Type ?u.6794
Set α: Type ?u.6784
α)) {empty_mem: ∅ ∈ B
empty_mem subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
subset_mem union_mem: ?m.6803
union_mem sUnion_univ: ∀ (x : α), {x} ∈ B
sUnion_univ} :
    @IsBounded: {α : Type ?u.6809} → [inst : Bornology α] → Set α → Prop
IsBounded _: Type ?u.6809
_ (ofBounded: {α : Type ?u.6811} →
  (B : Set (Set α)) →
    ∅ ∈ B →
      (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B) →
        (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B) → (∀ (x : α), {x} ∈ B) → Bornology α
ofBounded B: Set (Set α)
B empty_mem: ?m.6797
empty_mem subset_mem: ?m.6800
subset_mem union_mem: ?m.6803
union_mem sUnion_univ: ?m.6806
sUnion_univ) s: Set α
s ↔ s: Set α
s ∈ B: Set (Set α)
B := by
Goals accomplished! 🐙
  ι: Type ?u.6781

α: Type u_1

β: Type ?u.6787

s: Set α

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (x : α), {x} ∈ B

IsBounded s ↔ s ∈ Brw [ι: Type ?u.6781

α: Type u_1

β: Type ?u.6787

s: Set α

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (x : α), {x} ∈ B

IsBounded s ↔ s ∈ B@isBounded_def: ∀ {α : Type ?u.6870} [inst : Bornology α] {s : Set α}, IsBounded s ↔ sᶜ ∈ cobounded α
isBounded_def _: Type ?u.6870
_ (ofBounded: {α : Type ?u.6872} →
  (B : Set (Set α)) →
    ∅ ∈ B →
      (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B) →
        (∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B) → (∀ (x : α), {x} ∈ B) → Bornology α
ofBounded B: Set (Set α)
B empty_mem: ∅ ∈ B
empty_mem subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B
subset_mem union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B
union_mem sUnion_univ: ∀ (x : α), {x} ∈ B
sUnion_univ),ι: Type ?u.6781

α: Type u_1

β: Type ?u.6787

s: Set α

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (x : α), {x} ∈ B

sᶜ ∈ cobounded α ↔ s ∈ B ι: Type ?u.6781

α: Type u_1

β: Type ?u.6787

s: Set α

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (x : α), {x} ∈ B

IsBounded s ↔ s ∈ B← Filter.mem_sets: ∀ {α : Type ?u.6914} {f : Filter α} {s : Set α}, s ∈ f.sets ↔ s ∈ f
Filter.mem_sets,ι: Type ?u.6781

α: Type u_1

β: Type ?u.6787

s: Set α

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (x : α), {x} ∈ B

sᶜ ∈ (cobounded α).sets ↔ s ∈ B
   ι: Type ?u.6781

α: Type u_1

β: Type ?u.6787

s: Set α

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (x : α), {x} ∈ B

IsBounded s ↔ s ∈ BofBounded_cobounded_sets: ∀ {α : Type ?u.6929} (B : Set (Set α)) (empty_mem : ∅ ∈ B)
  (subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B)
  (union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B) (singleton_mem : ∀ (x : α), {x} ∈ B),
  (cobounded α).sets = { s | sᶜ ∈ B }
ofBounded_cobounded_sets,ι: Type ?u.6781

α: Type u_1

β: Type ?u.6787

s: Set α

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (x : α), {x} ∈ B

sᶜ ∈ { s | sᶜ ∈ B } ↔ s ∈ B ι: Type ?u.6781

α: Type u_1

β: Type ?u.6787

s: Set α

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (x : α), {x} ∈ B

IsBounded s ↔ s ∈ BSet.mem_setOf_eq: ∀ {α : Type ?u.6994} {x : α} {p : α → Prop}, (x ∈ { y | p y }) = p x
Set.mem_setOf_eq,ι: Type ?u.6781

α: Type u_1

β: Type ?u.6787

s: Set α

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (x : α), {x} ∈ B

sᶜᶜ ∈ B ↔ s ∈ B ι: Type ?u.6781

α: Type u_1

β: Type ?u.6787

s: Set α

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (x : α), {x} ∈ B

IsBounded s ↔ s ∈ Bcompl_compl: ∀ {α : Type ?u.7009} [inst : BooleanAlgebra α] (x : α), xᶜᶜ = x
compl_complι: Type ?u.6781

α: Type u_1

β: Type ?u.6787

s: Set α

B: Set (Set α)

empty_mem: ∅ ∈ B

subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B

union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B

sUnion_univ: ∀ (x : α), {x} ∈ B

s ∈ B ↔ s ∈ B]
Goals accomplished! 🐙
-- porting note: again had to use `@isBounded_def _` and feed Lean the instance
#align bornology.is_bounded_of_bounded_iff Bornology.isBounded_ofBounded_iff: ∀ {α : Type u_1} {s : Set α} (B : Set (Set α)) {empty_mem : ∅ ∈ B}
  {subset_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ B}
  {union_mem : ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ B} {sUnion_univ : ∀ (x : α), {x} ∈ B},
  IsBounded s ↔ s ∈ B
Bornology.isBounded_ofBounded_iff

variable [Bornology: Type ?u.7539 → Type ?u.7539
Bornology α: Type ?u.7090
α]

theorem isCobounded_biInter: ∀ {s : Set ι} {f : ι → Set α},
  Set.Finite s → (IsCobounded (iInter fun i => iInter fun h => f i) ↔ ∀ (i : ι), i ∈ s → IsCobounded (f i))
isCobounded_biInter {s: Set ι
s : Set: Type ?u.7117 → Type ?u.7117
Set ι: Type ?u.7102
ι} {f: ι → Set α
f : ι: Type ?u.7102
ι → Set: Type ?u.7122 → Type ?u.7122
Set α: Type ?u.7105
α} (hs: Set.Finite s
hs : s: Set ι
s.Finite: {α : Type ?u.7126} → Set α → Prop
Finite) :
    IsCobounded: {α : Type ?u.7133} → [inst : Bornology α] → Set α → Prop
IsCobounded (⋂ i: ?m.7143
i ∈ s: Set ι
s, f: ι → Set α
f i: ?m.7143
i) ↔ ∀ i: ?m.7201
i ∈ s: Set ι
s, IsCobounded: {α : Type ?u.7236} → [inst : Bornology α] → Set α → Prop
IsCobounded (f: ι → Set α
f i: ?m.7201
i) :=
  biInter_mem: ∀ {α : Type ?u.7252} {f : Filter α} {β : Type ?u.7251} {s : β → Set α} {is : Set β},
  Set.Finite is → ((iInter fun i => iInter fun h => s i) ∈ f ↔ ∀ (i : β), i ∈ is → s i ∈ f)
biInter_mem hs: Set.Finite s
hs
#align bornology.is_cobounded_bInter Bornology.isCobounded_biInter: ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] {s : Set ι} {f : ι → Set α},
  Set.Finite s → (IsCobounded (iInter fun i => iInter fun h => f i) ↔ ∀ (i : ι), i ∈ s → IsCobounded (f i))
Bornology.isCobounded_biInter

@[simp]
theorem isCobounded_biInter_finset: ∀ (s : Finset ι) {f : ι → Set α},
  IsCobounded (iInter fun i => iInter fun h => f i) ↔ ∀ (i : ι), i ∈ s → IsCobounded (f i)
isCobounded_biInter_finset (s: Finset ι
s : Finset: Type ?u.7324 → Type ?u.7324
Finset ι: Type ?u.7309
ι) {f: ι → Set α
f : ι: Type ?u.7309
ι → Set: Type ?u.7329 → Type ?u.7329
Set α: Type ?u.7312
α} :
    IsCobounded: {α : Type ?u.7333} → [inst : Bornology α] → Set α → Prop
IsCobounded (⋂ i: ?m.7343
i ∈ s: Finset ι
s, f: ι → Set α
f i: ?m.7343
i) ↔ ∀ i: ?m.7401
i ∈ s: Finset ι
s, IsCobounded: {α : Type ?u.7435} → [inst : Bornology α] → Set α → Prop
IsCobounded (f: ι → Set α
f i: ?m.7401
i) :=
  biInter_finset_mem: ∀ {α : Type ?u.7450} {f : Filter α} {β : Type ?u.7449} {s : β → Set α} (is : Finset β),
  (iInter fun i => iInter fun h => s i) ∈ f ↔ ∀ (i : β), i ∈ is → s i ∈ f
biInter_finset_mem s: Finset ι
s
#align bornology.is_cobounded_bInter_finset Bornology.isCobounded_biInter_finset: ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] (s : Finset ι) {f : ι → Set α},
  IsCobounded (iInter fun i => iInter fun h => f i) ↔ ∀ (i : ι), i ∈ s → IsCobounded (f i)
Bornology.isCobounded_biInter_finset

@[simp]
theorem isCobounded_iInter: ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] [inst_1 : Finite ι] {f : ι → Set α},
  IsCobounded (iInter fun i => f i) ↔ ∀ (i : ι), IsCobounded (f i)
isCobounded_iInter [Finite: Sort ?u.7542 → Prop
Finite ι: Type ?u.7527
ι] {f: ι → Set α
f : ι: Type ?u.7527
ι → Set: Type ?u.7547 → Type ?u.7547
Set α: Type ?u.7530
α} :
    IsCobounded: {α : Type ?u.7551} → [inst : Bornology α] → Set α → Prop
IsCobounded (⋂ i: ?m.7561
i, f: ι → Set α
f i: ?m.7561
i) ↔ ∀ i: ?m.7574
i, IsCobounded: {α : Type ?u.7577} → [inst : Bornology α] → Set α → Prop
IsCobounded (f: ι → Set α
f i: ?m.7574
i) :=
  iInter_mem: ∀ {α : Type ?u.7591} {f : Filter α} {β : Type ?u.7590} {s : β → Set α} [inst : Finite β],
  (iInter fun i => s i) ∈ f ↔ ∀ (i : β), s i ∈ f
iInter_mem
#align bornology.is_cobounded_Inter Bornology.isCobounded_iInter: ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] [inst_1 : Finite ι] {f : ι → Set α},
  IsCobounded (iInter fun i => f i) ↔ ∀ (i : ι), IsCobounded (f i)
Bornology.isCobounded_iInter

theorem isCobounded_sInter: ∀ {S : Set (Set α)}, Set.Finite S → (IsCobounded (⋂₀ S) ↔ ∀ (s : Set α), s ∈ S → IsCobounded s)
isCobounded_sInter {S: Set (Set α)
S : Set: Type ?u.7739 → Type ?u.7739
Set (Set: Type ?u.7740 → Type ?u.7740
Set α: Type ?u.7727
α)} (hs: Set.Finite S
hs : S: Set (Set α)
S.Finite: {α : Type ?u.7743} → Set α → Prop
Finite) :
    IsCobounded: {α : Type ?u.7750} → [inst : Bornology α] → Set α → Prop
IsCobounded (⋂₀ S: Set (Set α)
S) ↔ ∀ s: ?m.7764
s ∈ S: Set (Set α)
S, IsCobounded: {α : Type ?u.7802} → [inst : Bornology α] → Set α → Prop
IsCobounded s: ?m.7764
s :=
  sInter_mem: ∀ {α : Type ?u.7814} {f : Filter α} {s : Set (Set α)}, Set.Finite s → (⋂₀ s ∈ f ↔ ∀ (U : Set α), U ∈ s → U ∈ f)
sInter_mem hs: Set.Finite S
hs
#align bornology.is_cobounded_sInter Bornology.isCobounded_sInter: ∀ {α : Type u_1} [inst : Bornology α] {S : Set (Set α)},
  Set.Finite S → (IsCobounded (⋂₀ S) ↔ ∀ (s : Set α), s ∈ S → IsCobounded s)
Bornology.isCobounded_sInter

theorem isBounded_biUnion: ∀ {s : Set ι} {f : ι → Set α},
  Set.Finite s → (IsBounded (iUnion fun i => iUnion fun h => f i) ↔ ∀ (i : ι), i ∈ s → IsBounded (f i))
isBounded_biUnion {s: Set ι
s : Set: Type ?u.7860 → Type ?u.7860
Set ι: Type ?u.7845
ι} {f: ι → Set α
f : ι: Type ?u.7845
ι → Set: Type ?u.7865 → Type ?u.7865
Set α: Type ?u.7848
α} (hs: Set.Finite s
hs : s: Set ι
s.Finite: {α : Type ?u.7869} → Set α → Prop
Finite) :
    IsBounded: {α : Type ?u.7876} → [inst : Bornology α] → Set α → Prop
IsBounded (⋃ i: ?m.7886
i ∈ s: Set ι
s, f: ι → Set α
f i: ?m.7886
i) ↔ ∀ i: ?m.7944
i ∈ s: Set ι
s, IsBounded: {α : Type ?u.7979} → [inst : Bornology α] → Set α → Prop
IsBounded (f: ι → Set α
f i: ?m.7944
i) := by
Goals accomplished! 🐙
  ι: Type u_1

α: Type u_2

β: Type ?u.7851

s✝: Set α

inst✝: Bornology α

s: Set ι

f: ι → Set α

hs: Set.Finite s

IsBounded (iUnion fun i => iUnion fun h => f i) ↔ ∀ (i : ι), i ∈ s → IsBounded (f i)simp only [← isCobounded_compl_iff: ∀ {α : Type ?u.8007} [inst : Bornology α] {s : Set α}, IsCobounded (sᶜ) ↔ IsBounded s
isCobounded_compl_iff, compl_iUnion: ∀ {β : Type ?u.8024} {ι : Sort ?u.8025} (s : ι → Set β), (iUnion fun i => s i)ᶜ = iInter fun i => s iᶜ
compl_iUnion, isCobounded_biInter: ∀ {ι : Type ?u.8044} {α : Type ?u.8045} [inst : Bornology α] {s : Set ι} {f : ι → Set α},
  Set.Finite s → (IsCobounded (iInter fun i => iInter fun h => f i) ↔ ∀ (i : ι), i ∈ s → IsCobounded (f i))
isCobounded_biInter hs: Set.Finite s
hs]
Goals accomplished! 🐙
#align bornology.is_bounded_bUnion Bornology.isBounded_biUnion: ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] {s : Set ι} {f : ι → Set α},
  Set.Finite s → (IsBounded (iUnion fun i => iUnion fun h => f i) ↔ ∀ (i : ι), i ∈ s → IsBounded (f i))
Bornology.isBounded_biUnion

theorem isBounded_biUnion_finset: ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] (s : Finset ι) {f : ι → Set α},
  IsBounded (iUnion fun i => iUnion fun h => f i) ↔ ∀ (i : ι), i ∈ s → IsBounded (f i)
isBounded_biUnion_finset (s: Finset ι
s : Finset: Type ?u.8600 → Type ?u.8600
Finset ι: Type ?u.8585
ι) {f: ι → Set α
f : ι: Type ?u.8585
ι → Set: Type ?u.8605 → Type ?u.8605
Set α: Type ?u.8588
α} :
    IsBounded: {α : Type ?u.8609} → [inst : Bornology α] → Set α → Prop
IsBounded (⋃ i: ?m.8619
i ∈ s: Finset ι
s, f: ι → Set α
f i: ?m.8619
i) ↔ ∀ i: ?m.8677
i ∈ s: Finset ι
s, IsBounded: {α : Type ?u.8711} → [inst : Bornology α] → Set α → Prop
IsBounded (f: ι → Set α
f i: ?m.8677
i) :=
  isBounded_biUnion: ∀ {ι : Type ?u.8725} {α : Type ?u.8726} [inst : Bornology α] {s : Set ι} {f : ι → Set α},
  Set.Finite s → (IsBounded (iUnion fun i => iUnion fun h => f i) ↔ ∀ (i : ι), i ∈ s → IsBounded (f i))
isBounded_biUnion s: Finset ι
s.finite_toSet: ∀ {α : Type ?u.8767} (s : Finset α), Set.Finite ↑s
finite_toSet
#align bornology.is_bounded_bUnion_finset Bornology.isBounded_biUnion_finset: ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] (s : Finset ι) {f : ι → Set α},
  IsBounded (iUnion fun i => iUnion fun h => f i) ↔ ∀ (i : ι), i ∈ s → IsBounded (f i)
Bornology.isBounded_biUnion_finset

theorem isBounded_sUnion: ∀ {S : Set (Set α)}, Set.Finite S → (IsBounded (⋃₀ S) ↔ ∀ (s : Set α), s ∈ S → IsBounded s)
isBounded_sUnion {S: Set (Set α)
S : Set: Type ?u.8812 → Type ?u.8812
Set (Set: Type ?u.8813 → Type ?u.8813
Set α: Type ?u.8800
α)} (hs: Set.Finite S
hs : S: Set (Set α)
S.Finite: {α : Type ?u.8816} → Set α → Prop
Finite) :
    IsBounded: {α : Type ?u.8823} → [inst : Bornology α] → Set α → Prop
IsBounded (⋃₀ S: Set (Set α)
S) ↔ ∀ s: ?m.8837
s ∈ S: Set (Set α)
S, IsBounded: {α : Type ?u.8875} → [inst : Bornology α] → Set α → Prop
IsBounded s: ?m.8837
s := by
Goals accomplished! 🐙 ι: Type ?u.8797

α: Type u_1

β: Type ?u.8803

s: Set α

inst✝: Bornology α

S: Set (Set α)

hs: Set.Finite S

IsBounded (⋃₀ S) ↔ ∀ (s : Set α), s ∈ S → IsBounded srw [ι: Type ?u.8797

α: Type u_1

β: Type ?u.8803

s: Set α

inst✝: Bornology α

S: Set (Set α)

hs: Set.Finite S

IsBounded (⋃₀ S) ↔ ∀ (s : Set α), s ∈ S → IsBounded ssUnion_eq_biUnion: ∀ {α : Type ?u.8889} {s : Set (Set α)}, ⋃₀ s = iUnion fun i => iUnion fun _h => i
sUnion_eq_biUnion,ι: Type ?u.8797

α: Type u_1

β: Type ?u.8803

s: Set α

inst✝: Bornology α

S: Set (Set α)

hs: Set.Finite S

IsBounded (iUnion fun i => iUnion fun _h => i) ↔ ∀ (s : Set α), s ∈ S → IsBounded s ι: Type ?u.8797

α: Type u_1

β: Type ?u.8803

s: Set α

inst✝: Bornology α

S: Set (Set α)

hs: Set.Finite S

IsBounded (⋃₀ S) ↔ ∀ (s : Set α), s ∈ S → IsBounded sisBounded_biUnion: ∀ {ι : Type ?u.8904} {α : Type ?u.8905} [inst : Bornology α] {s : Set ι} {f : ι → Set α},
  Set.Finite s → (IsBounded (iUnion fun i => iUnion fun h => f i) ↔ ∀ (i : ι), i ∈ s → IsBounded (f i))
isBounded_biUnion hs: Set.Finite S
hsι: Type ?u.8797

α: Type u_1

β: Type ?u.8803

s: Set α

inst✝: Bornology α

S: Set (Set α)

hs: Set.Finite S

(∀ (i : Set α), i ∈ S → IsBounded i) ↔ ∀ (s : Set α), s ∈ S → IsBounded s]
Goals accomplished! 🐙
#align bornology.is_bounded_sUnion Bornology.isBounded_sUnion: ∀ {α : Type u_1} [inst : Bornology α] {S : Set (Set α)},
  Set.Finite S → (IsBounded (⋃₀ S) ↔ ∀ (s : Set α), s ∈ S → IsBounded s)
Bornology.isBounded_sUnion

@[simp]
theorem isBounded_iUnion: ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] [inst_1 : Finite ι] {s : ι → Set α},
  IsBounded (iUnion fun i => s i) ↔ ∀ (i : ι), IsBounded (s i)
isBounded_iUnion [Finite: Sort ?u.8990 → Prop
Finite ι: Type ?u.8975
ι] {s: ι → Set α
s : ι: Type ?u.8975
ι → Set: Type ?u.8995 → Type ?u.8995
Set α: Type ?u.8978
α} : IsBounded: {α : Type ?u.8999} → [inst : Bornology α] → Set α → Prop
IsBounded (⋃ i: ?m.9009
i, s: ι → Set α
s i: ?m.9009
i) ↔ ∀ i: ?m.9022
i, IsBounded: {α : Type ?u.9025} → [inst : Bornology α] → Set α → Prop
IsBounded (s: ι → Set α
s i: ?m.9022
i) :=
  by
Goals accomplished! 🐙 ι: Type u_1

α: Type u_2

β: Type ?u.8981

s✝: Set α

inst✝¹: Bornology α

inst✝: Finite ι

s: ι → Set α

IsBounded (iUnion fun i => s i) ↔ ∀ (i : ι), IsBounded (s i)rw [ι: Type u_1

α: Type u_2

β: Type ?u.8981

s✝: Set α

inst✝¹: Bornology α

inst✝: Finite ι

s: ι → Set α

IsBounded (iUnion fun i => s i) ↔ ∀ (i : ι), IsBounded (s i)← sUnion_range: ∀ {β : Type ?u.9040} {ι : Sort ?u.9041} (f : ι → Set β), ⋃₀ range f = iUnion fun x => f x
sUnion_range,ι: Type u_1

α: Type u_2

β: Type ?u.8981

s✝: Set α

inst✝¹: Bornology α

inst✝: Finite ι

s: ι → Set α

IsBounded (⋃₀ range fun i => s i) ↔ ∀ (i : ι), IsBounded (s i) ι: Type u_1

α: Type u_2

β: Type ?u.8981

s✝: Set α

inst✝¹: Bornology α

inst✝: Finite ι

s: ι → Set α

IsBounded (iUnion fun i => s i) ↔ ∀ (i : ι), IsBounded (s i)isBounded_sUnion: ∀ {α : Type ?u.9064} [inst : Bornology α] {S : Set (Set α)},
  Set.Finite S → (IsBounded (⋃₀ S) ↔ ∀ (s : Set α), s ∈ S → IsBounded s)
isBounded_sUnion (finite_range: ∀ {α : Type ?u.9069} {ι : Sort ?u.9068} (f : ι → α) [inst : Finite ι], Set.Finite (range f)
finite_range s: ι → Set α
s),ι: Type u_1

α: Type u_2

β: Type ?u.8981

s✝: Set α

inst✝¹: Bornology α

inst✝: Finite ι

s: ι → Set α

(∀ (s_1 : Set α), s_1 ∈ range s → IsBounded s_1) ↔ ∀ (i : ι), IsBounded (s i) ι: Type u_1

α: Type u_2

β: Type ?u.8981

s✝: Set α

inst✝¹: Bornology α

inst✝: Finite ι

s: ι → Set α

IsBounded (iUnion fun i => s i) ↔ ∀ (i : ι), IsBounded (s i)forall_range_iff: ∀ {α : Type ?u.9106} {ι : Sort ?u.9107} {f : ι → α} {p : α → Prop}, (∀ (a : α), a ∈ range f → p a) ↔ ∀ (i : ι), p (f i)
forall_range_iffι: Type u_1

α: Type u_2

β: Type ?u.8981

s✝: Set α

inst✝¹: Bornology α

inst✝: Finite ι

s: ι → Set α

(∀ (i : ι), IsBounded (s i)) ↔ ∀ (i : ι), IsBounded (s i)]
Goals accomplished! 🐙
#align bornology.is_bounded_Union Bornology.isBounded_iUnion: ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] [inst_1 : Finite ι] {s : ι → Set α},
  IsBounded (iUnion fun i => s i) ↔ ∀ (i : ι), IsBounded (s i)
Bornology.isBounded_iUnion

end Bornology

open Bornology

theorem Set.Finite.isBounded: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, Set.Finite s → IsBounded s
Set.Finite.isBounded [Bornology: Type ?u.9197 → Type ?u.9197
Bornology α: Type ?u.9191
α] {s: Set α
s : Set: Type ?u.9200 → Type ?u.9200
Set α: Type ?u.9191
α} (hs: Set.Finite s
hs : s: Set α
s.Finite: {α : Type ?u.9203} → Set α → Prop
Finite) : IsBounded: {α : Type ?u.9210} → [inst : Bornology α] → Set α → Prop
IsBounded s: Set α
s :=
  Bornology.le_cofinite: ∀ (α : Type ?u.9227) [inst : Bornology α], cobounded α ≤ cofinite
Bornology.le_cofinite α: Type ?u.9191
α hs: Set.Finite s
hs.compl_mem_cofinite: ∀ {α : Type ?u.9238} {s : Set α}, Set.Finite s → sᶜ ∈ cofinite
compl_mem_cofinite
#align set.finite.is_bounded Set.Finite.isBounded: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, Set.Finite s → IsBounded s
Set.Finite.isBounded

instance: Bornology PUnit
instance : Bornology: Type ?u.9261 → Type ?u.9261
Bornology PUnit: Sort ?u.9262
PUnit :=
  ⟨⊥: ?m.9271
⊥, bot_le: ∀ {α : Type ?u.9328} [inst : LE α] [inst_1 : OrderBot α] {a : α}, ⊥ ≤ a
bot_le⟩

/-- The cofinite filter as a bornology -/
@[reducible]
def Bornology.cofinite: Bornology α
Bornology.cofinite : Bornology: Type ?u.9865 → Type ?u.9865
Bornology α: Type ?u.9859
α
    where
  cobounded' := Filter.cofinite: {α : Type ?u.9870} → Filter α
Filter.cofinite
  le_cofinite' := le_rfl: ∀ {α : Type ?u.9873} [inst : Preorder α] {a : α}, a ≤ a
le_rfl
#align bornology.cofinite Bornology.cofinite: {α : Type u_1} → Bornology α
Bornology.cofinite

/-- A space with a `Bornology` is a **bounded space** if `Set.univ : Set α` is bounded. -/
class BoundedSpace: ∀ {α : Type u_1} [inst : Bornology α], IsBounded univ → BoundedSpace α
BoundedSpace (α: Type ?u.10021
α : Type _: Type (?u.10021+1)
Type _) [Bornology: Type ?u.10024 → Type ?u.10024
Bornology α: Type ?u.10021
α] : Prop: Type
Prop where
  /-- The `Set.univ` is bounded. -/
  bounded_univ: ∀ {α : Type u_1} [inst : Bornology α] [self : BoundedSpace α], IsBounded univ
bounded_univ : Bornology.IsBounded: {α : Type ?u.10028} → [inst : Bornology α] → Set α → Prop
Bornology.IsBounded (univ: {α : Type ?u.10036} → Set α
univ : Set: Type ?u.10035 → Type ?u.10035
Set α: Type ?u.10021
α)
#align bounded_space BoundedSpace: (α : Type u_1) → [inst : Bornology α] → Prop
BoundedSpace

namespace Bornology

variable [Bornology: Type ?u.10343 → Type ?u.10343
Bornology α: Type ?u.10057
α]

theorem isBounded_univ: ∀ {α : Type u_1} [inst : Bornology α], IsBounded univ ↔ BoundedSpace α
isBounded_univ : IsBounded: {α : Type ?u.10078} → [inst : Bornology α] → Set α → Prop
IsBounded (univ: {α : Type ?u.10083} → Set α
univ : Set: Type ?u.10082 → Type ?u.10082
Set α: Type ?u.10069
α) ↔ BoundedSpace: (α : Type ?u.10090) → [inst : Bornology α] → Prop
BoundedSpace α: Type ?u.10069
α :=
  ⟨fun h: ?m.10102
h => ⟨h: ?m.10102
h⟩, fun h: ?m.10125
h => h: ?m.10125
h.1: ∀ {α : Type ?u.10127} [inst : Bornology α] [self : BoundedSpace α], IsBounded univ
1⟩
#align bornology.is_bounded_univ Bornology.isBounded_univ: ∀ {α : Type u_1} [inst : Bornology α], IsBounded univ ↔ BoundedSpace α
Bornology.isBounded_univ

theorem cobounded_eq_bot_iff: ∀ {α : Type u_1} [inst : Bornology α], cobounded α = ⊥ ↔ BoundedSpace α
cobounded_eq_bot_iff : cobounded: (α : Type ?u.10151) → [inst : Bornology α] → Filter α
cobounded α: Type ?u.10141
α = ⊥: ?m.10157
⊥ ↔ BoundedSpace: (α : Type ?u.10238) → [inst : Bornology α] → Prop
BoundedSpace α: Type ?u.10141
α := by
Goals accomplished! 🐙
  ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α

cobounded α = ⊥ ↔ BoundedSpace αrw [ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α

cobounded α = ⊥ ↔ BoundedSpace α← isBounded_univ: ∀ {α : Type ?u.10242} [inst : Bornology α], IsBounded univ ↔ BoundedSpace α
isBounded_univ,ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α

cobounded α = ⊥ ↔ IsBounded univ ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α

cobounded α = ⊥ ↔ BoundedSpace αisBounded_def: ∀ {α : Type ?u.10257} [inst : Bornology α] {s : Set α}, IsBounded s ↔ sᶜ ∈ cobounded α
isBounded_def,ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α

cobounded α = ⊥ ↔ univᶜ ∈ cobounded α ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α

cobounded α = ⊥ ↔ BoundedSpace αcompl_univ: ∀ {α : Type ?u.10274}, univᶜ = ∅
compl_univ,ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α

cobounded α = ⊥ ↔ ∅ ∈ cobounded α ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α

cobounded α = ⊥ ↔ BoundedSpace αempty_mem_iff_bot: ∀ {α : Type ?u.10286} {f : Filter α}, ∅ ∈ f ↔ f = ⊥
empty_mem_iff_botι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α

cobounded α = ⊥ ↔ cobounded α = ⊥]
Goals accomplished! 🐙
#align bornology.cobounded_eq_bot_iff Bornology.cobounded_eq_bot_iff: ∀ {α : Type u_1} [inst : Bornology α], cobounded α = ⊥ ↔ BoundedSpace α
Bornology.cobounded_eq_bot_iff

variable [BoundedSpace: (α : Type ?u.10542) → [inst : Bornology α] → Prop
BoundedSpace α: Type ?u.10318
α]

theorem IsBounded.all: ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : BoundedSpace α] (s : Set α), IsBounded s
IsBounded.all (s: Set α
s : Set: Type ?u.10353 → Type ?u.10353
Set α: Type ?u.10337
α) : IsBounded: {α : Type ?u.10356} → [inst : Bornology α] → Set α → Prop
IsBounded s: Set α
s :=
  BoundedSpace.bounded_univ: ∀ {α : Type ?u.10371} [inst : Bornology α] [self : BoundedSpace α], IsBounded univ
BoundedSpace.bounded_univ.subset: ∀ {α : Type ?u.10381} [inst : Bornology α] {s t : Set α}, IsBounded t → s ⊆ t → IsBounded s
subset s: Set α
s.subset_univ: ∀ {α : Type ?u.10406} (s : Set α), s ⊆ univ
subset_univ
#align bornology.is_bounded.all Bornology.IsBounded.all: ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : BoundedSpace α] (s : Set α), IsBounded s
Bornology.IsBounded.all

theorem IsCobounded.all: ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : BoundedSpace α] (s : Set α), IsCobounded s
IsCobounded.all (s: Set α
s : Set: Type ?u.10446 → Type ?u.10446
Set α: Type ?u.10430
α) : IsCobounded: {α : Type ?u.10449} → [inst : Bornology α] → Set α → Prop
IsCobounded s: Set α
s :=
  compl_compl: ∀ {α : Type ?u.10464} [inst : BooleanAlgebra α] (x : α), xᶜᶜ = x
compl_compl s: Set α
s ▸ IsBounded.all: ∀ {α : Type ?u.10475} [inst : Bornology α] [inst_1 : BoundedSpace α] (s : Set α), IsBounded s
IsBounded.all (s: Set α
sᶜ)
#align bornology.is_cobounded.all Bornology.IsCobounded.all: ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : BoundedSpace α] (s : Set α), IsCobounded s
Bornology.IsCobounded.all

variable (α: ?m.10549
α)

@[simp]
theorem cobounded_eq_bot: ∀ (α : Type u_1) [inst : Bornology α] [inst_1 : BoundedSpace α], cobounded α = ⊥
cobounded_eq_bot : cobounded: (α : Type ?u.10572) → [inst : Bornology α] → Filter α
cobounded α: Type ?u.10555
α = ⊥: ?m.10578
⊥ :=
  cobounded_eq_bot_iff: ∀ {α : Type ?u.10660} [inst : Bornology α], cobounded α = ⊥ ↔ BoundedSpace α
cobounded_eq_bot_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 ‹_›
#align bornology.cobounded_eq_bot Bornology.cobounded_eq_bot: ∀ (α : Type u_1) [inst : Bornology α] [inst_1 : BoundedSpace α], cobounded α = ⊥
Bornology.cobounded_eq_bot

end Bornology