Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
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_1Bornology (α: 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.25Filter α: 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' ≤ cofinitele_cofinite' : cobounded': Filter αcobounded' ≤ cofinite: {α : Type ?u.29} → Filter αcofinite
#align bornology Bornology: Type u_1 → Type u_1Bornology

/- 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.114Bornology α: Type ?u.111α] : Filter: Type ?u.117 → Type ?u.117Filter α: 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 α ≤ cofiniteBornology.le_cofinite (α: Type u_1α : Type _: Type (?u.175+1)Type _) [Bornology: Type ?u.178 → Type ?u.178Bornology α: 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' ≤ cofiniteBornology.le_cofinite'
#align bornology.le_cofinite Bornology.le_cofinite: ∀ (α : Type u_1) [inst : Bornology α], Bornology.cobounded α ≤ cofiniteBornology.le_cofinite

initialize_simps_projections Bornology: Type u_1 → Type u_1Bornology (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.301Bornology α: 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' := byGoals accomplished! 🐙
ι: Type ?u.289α: Type u_1β: Type ?u.295t, t': Bornology αh_cobounded: cobounded α = cobounded αt = t'cases t: Bornology αtι: Type ?u.289α: Type u_1β: Type ?u.295t': Bornology αcobounded'✝: Filter αle_cofinite'✝: cobounded'✝ ≤ cofiniteh_cobounded: cobounded α = cobounded αmk{ cobounded' := cobounded'✝, le_cofinite' := le_cofinite'✝ } = t'
ι: Type ?u.289α: Type u_1β: Type ?u.295t, t': Bornology αh_cobounded: cobounded α = cobounded αt = t'cases t': Bornology αt'ι: Type ?u.289α: Type u_1β: Type ?u.295cobounded'✝¹: Filter αle_cofinite'✝¹: cobounded'✝¹ ≤ cofinitecobounded'✝: Filter αle_cofinite'✝: cobounded'✝ ≤ cofiniteh_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.295t, t': Bornology αh_cobounded: cobounded α = cobounded αt = t'congrGoals 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.612Bornology α: 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.675Set (Set: Type ?u.676 → Type ?u.676Set α: Type ?u.672α))
(empty_mem: ∅ ∈ Bempty_mem : ∅: ?m.701∅ ∈ B: Set (Set α)B)
(subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bsubset_mem : ∀ s₁: ?m.792s₁ (_: s₁ ∈ B_ : s₁: ?m.792s₁ ∈ B: Set (Set α)B) s₂: ?m.827s₂, s₂: ?m.827s₂ ⊆ s₁: ?m.792s₁ → s₂: ?m.827s₂ ∈ B: Set (Set α)B)
(union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bunion_mem : ∀ s₁: ?m.884s₁ (_: s₁ ∈ B_ : s₁: ?m.884s₁ ∈ B: Set (Set α)B) s₂: ?m.919s₂ (_: s₂ ∈ B_ : s₂: ?m.919s₂ ∈ B: Set (Set α)B), s₁: ?m.884s₁ ∪ s₂: ?m.919s₂ ∈ B: Set (Set α)B)
(singleton_mem: ∀ (x : ?m.1001), ?m.1064 x ∈ Bsingleton_mem : ∀ x: ?m.1001x, {x: ?m.1001x} ∈ B: Set (Set α)B) : Bornology: Type ?u.1068 → Type ?u.1068Bornology α: Type ?u.672α
where
cobounded' :=
{ sets := { s: Set αs : Set: Type ?u.1127 → Type ?u.1127Set α: Type ?u.672α | s: Set αsᶜ ∈ B: Set (Set α)B }
univ_sets := byGoals accomplished! 🐙 ι: Type ?u.663α✝: Type ?u.666β: Type ?u.669α: Type ?u.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_mem: ∀ (x : α), {x} ∈ Buniv ∈ { s | sᶜ ∈ B }rwa [ι: Type ?u.663α✝: Type ?u.666β: Type ?u.669α: Type ?u.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_mem: ∀ (x : α), {x} ∈ Buniv ∈ { s | sᶜ ∈ B }← compl_univ: ∀ {α : Type ?u.1278}, univᶜ = ∅compl_univι: Type ?u.663α✝: Type ?u.666β: Type ?u.669α: Type ?u.672B: Set (Set α)empty_mem: univᶜ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_mem: ∀ (x : α), {x} ∈ Buniv ∈ { s | sᶜ ∈ B }]ι: Type ?u.663α✝: Type ?u.666β: Type ?u.669α: Type ?u.672B: Set (Set α)empty_mem: univᶜ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_mem: ∀ (x : α), {x} ∈ Buniv ∈ { s | sᶜ ∈ B } at empty_mem: ∅ ∈ Bempty_memGoals accomplished! 🐙
sets_of_superset := fun hx: ?m.1175hx hy: ?m.1178hy => subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bsubset_mem _: Set α_ hx: ?m.1175hx _: Set α_ (compl_subset_compl: ∀ {α : Type ?u.1207} {s t : Set α}, sᶜ ⊆ tᶜ ↔ t ⊆ scompl_subset_compl.mpr: ∀ {a b : Prop}, (a ↔ b) → b → ampr hy: ?m.1178hy)
inter_sets := fun hx: ?m.1252hx hy: ?m.1255hy => byGoals accomplished! 🐙 ι: Type ?u.663α✝: Type ?u.666β: Type ?u.669α: Type ?u.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_mem: ∀ (x : α), {x} ∈ Bx✝, 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₂ ∈ Bunion_mem _: Set α_ hx: x✝ ∈ { s | sᶜ ∈ B }hx _: Set α_ hy: y✝ ∈ { s | sᶜ ∈ B }hyGoals accomplished! 🐙 }
le_cofinite' := byGoals accomplished! 🐙
ι: Type ?u.663α✝: Type ?u.666β: Type ?u.669α: Type ?u.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_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.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_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}ᶜ ∈ lle_cofinite_iff_compl_singleton_memι: Type ?u.663α✝: Type ?u.666β: Type ?u.669α: Type ?u.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_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.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_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.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_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.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_mem: ∀ (x : α), {x} ∈ Bx: α{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.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_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.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_mem: ∀ (x : α), {x} ∈ Bx: α{x}ᶜᶜ ∈ B
ι: Type ?u.663α✝: Type ?u.666β: Type ?u.669α: Type ?u.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_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.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_mem: ∀ (x : α), {x} ∈ Bx: α{x}ᶜᶜ ∈ Bcompl_compl: ∀ {α : Type ?u.2208} [inst : BooleanAlgebra α] (x : α), xᶜᶜ = xcompl_complι: Type ?u.663α✝: Type ?u.666β: Type ?u.669α: Type ?u.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_mem: ∀ (x : α), {x} ∈ Bx: α{x} ∈ B]ι: Type ?u.663α✝: Type ?u.666β: Type ?u.669α: Type ?u.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_mem: ∀ (x : α), {x} ∈ Bx: α{x} ∈ B
ι: Type ?u.663α✝: Type ?u.666β: Type ?u.669α: Type ?u.672B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bsingleton_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} ∈ Bsingleton_mem x: αxGoals 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.2570Set (Set: Type ?u.2571 → Type ?u.2571Set α: Type ?u.2567α))
(empty_mem: ∅ ∈ Bempty_mem : ∅: ?m.2596∅ ∈ B: Set (Set α)B)
(subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bsubset_mem : ∀ s₁: ?m.2687s₁ (_: s₁ ∈ B_ : s₁: ?m.2687s₁ ∈ B: Set (Set α)B) s₂: ?m.2722s₂, s₂: ?m.2722s₂ ⊆ s₁: ?m.2687s₁ → s₂: ?m.2722s₂ ∈ B: Set (Set α)B)
(union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bunion_mem : ∀ s₁: ?m.2779s₁ (_: s₁ ∈ B_ : s₁: ?m.2779s₁ ∈ B: Set (Set α)B) s₂: ?m.2814s₂ (_: s₂ ∈ B_ : s₂: ?m.2814s₂ ∈ B: Set (Set α)B), s₁: ?m.2779s₁ ∪ s₂: ?m.2814s₂ ∈ B: Set (Set α)B)
(sUnion_univ: ⋃₀ B = univsUnion_univ : ⋃₀ B: Set (Set α)B = univ: {α : Type ?u.2901} → Set αuniv) :
Bornology: Type ?u.2934 → Type ?u.2934Bornology α: 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: ∅ ∈ Bempty_mem subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bsubset_mem union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bunion_mem fun x: ?m.2984x => byGoals accomplished! 🐙
ι: Type ?u.2558α✝: Type ?u.2561β: Type ?u.2564α: Type ?u.2567B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ⋃₀ B = univx: α{x} ∈ Brw [ι: Type ?u.2558α✝: Type ?u.2561β: Type ?u.2564α: Type ?u.2567B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ⋃₀ B = univx: α{x} ∈ BsUnion_eq_univ_iff: ∀ {α : Type ?u.2991} {c : Set (Set α)}, ⋃₀ c = univ ↔ ∀ (a : α), ∃ b, b ∈ c ∧ a ∈ bsUnion_eq_univ_iffι: Type ?u.2558α✝: Type ?u.2561β: Type ?u.2564α: Type ?u.2567B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (a : α), ∃ b, b ∈ B ∧ a ∈ bx: α{x} ∈ B]ι: Type ?u.2558α✝: Type ?u.2561β: Type ?u.2564α: Type ?u.2567B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (a : α), ∃ b, b ∈ B ∧ a ∈ bx: α{x} ∈ B at sUnion_univ: ⋃₀ B = univsUnion_univι: Type ?u.2558α✝: Type ?u.2561β: Type ?u.2564α: Type ?u.2567B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (a : α), ∃ b, b ∈ B ∧ a ∈ bx: α{x} ∈ B
ι: Type ?u.2558α✝: Type ?u.2561β: Type ?u.2564α: Type ?u.2567B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ⋃₀ B = univx: α{x} ∈ Brcases sUnion_univ: ∀ (a : α), ∃ b, b ∈ B ∧ a ∈ bsUnion_univ x: αx with ⟨s, hs, hxs⟩: s ∈ B ∧ x ∈ s⟨s: Set αs⟨s, hs, hxs⟩: s ∈ B ∧ x ∈ s, hs: s ∈ Bhs⟨s, hs, hxs⟩: s ∈ B ∧ x ∈ s, hxs: x ∈ shxs⟨s, hs, hxs⟩: s ∈ B ∧ x ∈ s⟩ι: Type ?u.2558α✝: Type ?u.2561β: Type ?u.2564α: Type ?u.2567B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (a : α), ∃ b, b ∈ B ∧ a ∈ bx: αs: Set αhs: s ∈ Bhxs: x ∈ sintro.intro{x} ∈ B
ι: Type ?u.2558α✝: Type ?u.2561β: Type ?u.2564α: Type ?u.2567B: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ⋃₀ B = univx: α{x} ∈ Bexact subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bsubset_mem s: Set αs hs: s ∈ Bhs {x: αx} (singleton_subset_iff: ∀ {α : Type ?u.3100} {a : α} {s : Set α}, {a} ⊆ s ↔ a ∈ ssingleton_subset_iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → ampr hxs: x ∈ shxs)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.3908Bornology α: Type ?u.3902α] {s: Set αs t: Set αt : Set: Type ?u.3782 → Type ?u.3782Set α: 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 α → PropIsCobounded (s: Set αs : Set: Type ?u.3737 → Type ?u.3737Set α: Type ?u.3720α) : Prop: TypeProp :=
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 α → PropBornology.IsCobounded

/-- `IsBounded` is the predicate that `s` is bounded relative to the ambient bornology on `α`. -/
def IsBounded: Set α → PropIsBounded (s: Set αs : Set: Type ?u.3790 → Type ?u.3790Set α: Type ?u.3773α) : Prop: TypeProp :=
IsCobounded: {α : Type ?u.3795} → [inst : Bornology α] → Set α → PropIsCobounded (s: Set αsᶜ)
#align bornology.is_bounded Bornology.IsBounded: {α : Type u_1} → [inst : Bornology α] → Set α → PropBornology.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.3860Set α: Type ?u.3843α} : IsCobounded: {α : Type ?u.3863} → [inst : Bornology α] → Set α → PropIsCobounded s: Set αs ↔ s: Set αs ∈ cobounded: (α : Type ?u.3878) → [inst : Bornology α] → Filter αcobounded α: Type ?u.3843α :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.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.3919Set α: Type ?u.3902α} : IsBounded: {α : Type ?u.3922} → [inst : Bornology α] → Set α → PropIsBounded s: Set αs ↔ s: Set αsᶜ ∈ cobounded: (α : Type ?u.3966) → [inst : Bornology α] → Filter αcobounded α: Type ?u.3902α :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.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 sisBounded_compl_iff : IsBounded: {α : Type ?u.4007} → [inst : Bornology α] → Set α → PropIsBounded (s: Set αsᶜ) ↔ IsCobounded: {α : Type ?u.4045} → [inst : Bornology α] → Set α → PropIsCobounded s: Set αs := byGoals accomplished! 🐙
ι: Type ?u.3987α: Type u_1β: Type ?u.3993inst✝: Bornology αs, t: Set αx: αIsBounded (sᶜ) ↔ IsCobounded srw [ι: Type ?u.3987α: Type u_1β: Type ?u.3993inst✝: 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.3993inst✝: Bornology αs, t: Set αx: αsᶜᶜ ∈ cobounded α ↔ IsCobounded s ι: Type ?u.3987α: Type u_1β: Type ?u.3993inst✝: 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.3993inst✝: Bornology αs, t: Set αx: αsᶜᶜ ∈ cobounded α ↔ s ∈ cobounded α ι: Type ?u.3987α: Type u_1β: Type ?u.3993inst✝: Bornology αs, t: Set αx: αIsBounded (sᶜ) ↔ IsCobounded scompl_compl: ∀ {α : Type ?u.4083} [inst : BooleanAlgebra α] (x : α), xᶜᶜ = xcompl_complι: Type ?u.3987α: Type u_1β: Type ?u.3993inst✝: 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 sBornology.isBounded_compl_iff

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

alias isBounded_compl_iff: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsBounded (sᶜ) ↔ IsCobounded sisBounded_compl_iff ↔ IsBounded.of_compl: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsBounded (sᶜ) → IsCobounded sIsBounded.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 sBornology.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 sisCobounded_compl_iff ↔ IsCobounded.of_compl: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, IsCobounded (sᶜ) → IsBounded sIsCobounded.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 sBornology.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 α → PropIsBounded (∅: ?m.4299∅ : Set: Type ?u.4297 → Type ?u.4297Set α: Type ?u.4274α) := byGoals accomplished! 🐙
ι: Type ?u.4271α: Type u_1β: Type ?u.4277inst✝: Bornology αs, t: Set αx: αIsBounded ∅rw [ι: Type ?u.4271α: Type u_1β: Type ?u.4277inst✝: 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.4277inst✝: Bornology αs, t: Set αx: α∅ᶜ ∈ cobounded α ι: Type ?u.4271α: Type u_1β: Type ?u.4277inst✝: Bornology αs, t: Set αx: αIsBounded ∅compl_empty: ∀ {α : Type ?u.4367}, ∅ᶜ = univcompl_emptyι: Type ?u.4271α: Type u_1β: Type ?u.4277inst✝: Bornology αs, t: Set αx: αuniv ∈ cobounded α]ι: Type ?u.4271α: Type u_1β: Type ?u.4277inst✝: Bornology αs, t: Set αx: αuniv ∈ cobounded α
ι: Type ?u.4271α: Type u_1β: Type ?u.4277inst✝: Bornology αs, t: Set αx: αIsBounded ∅exact univ_mem: ∀ {α : Type ?u.4385} {f : Filter α}, univ ∈ funiv_memGoals 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 α → PropIsBounded ({x: αx} : Set: Type ?u.4441 → Type ?u.4441Set α: Type ?u.4418α) := byGoals accomplished! 🐙
ι: Type ?u.4415α: Type u_1β: Type ?u.4421inst✝: Bornology αs, t: Set αx: αIsBounded {x}rw [ι: Type ?u.4415α: Type u_1β: Type ?u.4421inst✝: 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.4421inst✝: Bornology αs, t: Set αx: α{x}ᶜ ∈ cobounded α]ι: Type ?u.4415α: Type u_1β: Type ?u.4421inst✝: Bornology αs, t: Set αx: α{x}ᶜ ∈ cobounded α
ι: Type ?u.4415α: Type u_1β: Type ?u.4421inst✝: Bornology αs, t: Set αx: αIsBounded {x}exact le_cofinite: ∀ (α : Type ?u.4494) [inst : Bornology α], cobounded α ≤ cofinitele_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ᶜ ∈ cofinitecompl_mem_cofiniteGoals 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 univisCobounded_univ : IsCobounded: {α : Type ?u.4565} → [inst : Bornology α] → Set α → PropIsCobounded (univ: {α : Type ?u.4572} → Set αuniv : Set: Type ?u.4571 → Type ?u.4571Set α: Type ?u.4548α) :=
univ_mem: ∀ {α : Type ?u.4580} {f : Filter α}, univ ∈ funiv_mem
#align bornology.is_cobounded_univ Bornology.isCobounded_univ: ∀ {α : Type u_1} [inst : Bornology α], IsCobounded univBornology.isCobounded_univ

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

theorem IsCobounded.inter: IsCobounded s → IsCobounded t → IsCobounded (s ∩ t)IsCobounded.inter (hs: IsCobounded shs : IsCobounded: {α : Type ?u.4738} → [inst : Bornology α] → Set α → PropIsCobounded s: Set αs) (ht: IsCobounded tht : IsCobounded: {α : Type ?u.4751} → [inst : Bornology α] → Set α → PropIsCobounded t: Set αt) : IsCobounded: {α : Type ?u.4760} → [inst : Bornology α] → Set α → PropIsCobounded (s: Set αs ∩ t: Set αt) :=
isCobounded_inter: ∀ {α : Type ?u.4790} [inst : Bornology α] {s t : Set α}, IsCobounded (s ∩ t) ↔ IsCobounded s ∧ IsCobounded tisCobounded_inter.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 ⟨hs: IsCobounded shs, ht: IsCobounded tht⟩
#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 tisBounded_union : IsBounded: {α : Type ?u.4848} → [inst : Bornology α] → Set α → PropIsBounded (s: Set αs ∪ t: Set αt) ↔ IsBounded: {α : Type ?u.4875} → [inst : Bornology α] → Set α → PropIsBounded s: Set αs ∧ IsBounded: {α : Type ?u.4880} → [inst : Bornology α] → Set α → PropIsBounded t: Set αt := byGoals accomplished! 🐙
ι: Type ?u.4828α: Type u_1β: Type ?u.4834inst✝: 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 sisCobounded_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 tisCobounded_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 tBornology.isBounded_union

theorem IsBounded.union: IsBounded s → IsBounded t → IsBounded (s ∪ t)IsBounded.union (hs: IsBounded shs : IsBounded: {α : Type ?u.5132} → [inst : Bornology α] → Set α → PropIsBounded s: Set αs) (ht: IsBounded tht : IsBounded: {α : Type ?u.5145} → [inst : Bornology α] → Set α → PropIsBounded t: Set αt) : IsBounded: {α : Type ?u.5154} → [inst : Bornology α] → Set α → PropIsBounded (s: Set αs ∪ t: Set αt) :=
isBounded_union: ∀ {α : Type ?u.5184} [inst : Bornology α] {s t : Set α}, IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded tisBounded_union.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 ⟨hs: IsBounded shs, ht: IsBounded tht⟩
#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 tIsCobounded.superset (hs: IsCobounded shs : IsCobounded: {α : Type ?u.5242} → [inst : Bornology α] → Set α → PropIsCobounded s: Set αs) (ht: s ⊆ tht : s: Set αs ⊆ t: Set αt) : IsCobounded: {α : Type ?u.5275} → [inst : Bornology α] → Set α → PropIsCobounded t: Set αt :=
mem_of_superset: ∀ {α : Type ?u.5287} {f : Filter α} {x y : Set α}, x ∈ f → x ⊆ y → y ∈ fmem_of_superset hs: IsCobounded shs ht: s ⊆ tht
#align bornology.is_cobounded.superset Bornology.IsCobounded.superset: ∀ {α : Type u_1} [inst : Bornology α] {s t : Set α}, IsCobounded s → s ⊆ t → IsCobounded tBornology.IsCobounded.superset

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

@[simp]
theorem sUnion_bounded_univ: ∀ {α : Type u_1} [inst : Bornology α], ⋃₀ { s | IsBounded s } = univsUnion_bounded_univ : ⋃₀ { s: Set αs : Set: Type ?u.5449 → Type ?u.5449Set α: Type ?u.5424α | IsBounded: {α : Type ?u.5452} → [inst : Bornology α] → Set α → PropIsBounded 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 ∈ bsUnion_eq_univ_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 fun a: ?m.5514a => ⟨{a: ?m.5514a}, isBounded_singleton: ∀ {α : Type ?u.5561} [inst : Bornology α] {x : α}, IsBounded {x}isBounded_singleton, mem_singleton: ∀ {α : Type ?u.5599} (a : α), a ∈ {a}mem_singleton a: ?m.5514a⟩
#align bornology.sUnion_bounded_univ Bornology.sUnion_bounded_univ: ∀ {α : Type u_1} [inst : Bornology α], ⋃₀ { s | IsBounded s } = univBornology.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.5644Bornology β: 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.5709s⦄, IsBounded: {α : Type ?u.5713} → [inst : Bornology α] → Set α → PropIsBounded s: ?m.5709s → IsBounded: {α : Type ?u.5723} → [inst : Bornology α] → Set α → PropIsBounded (f: α → βf '' s: ?m.5709s) := byGoals accomplished! 🐙
ι: Type ?u.5624α: Type u_2β: Type u_1inst✝¹: Bornology αs, t: Set αx: αinst✝: Bornology βf: α → βcomap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)refine'
⟨fun h: ?m.5762h s: ?m.5765s hs: ?m.5768hs => _: IsBounded (f '' s)_, fun h: ?m.5777h t: ?m.5782t ht: ?m.5785ht =>
⟨(f: α → βf '' t: ?m.5782tᶜ)ᶜ, h: ?m.5777h <| IsCobounded.compl: ∀ {α : Type ?u.5892} [inst : Bornology α] {s : Set α}, IsCobounded s → IsBounded (sᶜ)IsCobounded.compl ht: ?m.5785ht, compl_subset_comm: ∀ {α : Type ?u.5908} {s t : Set α}, sᶜ ⊆ t ↔ tᶜ ⊆ scompl_subset_comm.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 <| 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_1inst✝¹: Bornology αs✝, t: Set αx: αinst✝: Bornology βf: α → βh: comap f (cobounded β) ≤ cobounded αs: Set αhs: IsBounded sIsBounded (f '' s)
ι: Type ?u.5624α: Type u_2β: Type u_1inst✝¹: 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.5762h hs: ?m.5768hs.compl: ∀ {α : Type ?u.5980} [inst : Bornology α] {s : Set α}, IsBounded s → IsCobounded (sᶜ)complι: Type ?u.5624α: Type u_2β: Type u_1inst✝¹: Bornology αs✝, t✝: Set αx: αinst✝: Bornology βf: α → βh: comap f (cobounded β) ≤ cobounded αs: Set αhs: IsBounded st: Set βht: t ∈ cobounded βhts: f ⁻¹' t ⊆ sᶜintro.introIsBounded (f '' s)
ι: Type ?u.5624α: Type u_2β: Type u_1inst✝¹: 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_1inst✝¹: Bornology αs✝, t✝: Set αx: αinst✝: Bornology βf: α → βh: comap f (cobounded β) ≤ cobounded αs: Set αhs: IsBounded st: 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_1inst✝¹: Bornology αs✝, t✝: Set αx: αinst✝: Bornology βf: α → βh: comap f (cobounded β) ≤ cobounded αs: Set αhs: IsBounded st: Set βht: t ∈ cobounded βhts: s ⊆ (f ⁻¹' t)ᶜintro.introIsBounded (f '' s) ι: Type ?u.5624α: Type u_2β: Type u_1inst✝¹: Bornology αs✝, t✝: Set αx: αinst✝: Bornology βf: α → βh: comap f (cobounded β) ≤ cobounded αs: Set αhs: IsBounded st: 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_1inst✝¹: Bornology αs✝, t✝: Set αx: αinst✝: Bornology βf: α → βh: comap f (cobounded β) ≤ cobounded αs: Set αhs: IsBounded st: Set βht: t ∈ cobounded βhts: s ⊆ f ⁻¹' tᶜintro.introIsBounded (f '' s)]ι: Type ?u.5624α: Type u_2β: Type u_1inst✝¹: Bornology αs✝, t✝: Set αx: αinst✝: Bornology βf: α → βh: comap f (cobounded β) ≤ cobounded αs: Set αhs: IsBounded st: 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_1inst✝¹: Bornology αs✝, t✝: Set αx: αinst✝: Bornology βf: α → βh: comap f (cobounded β) ≤ cobounded αs: Set αhs: IsBounded st: Set βht: t ∈ cobounded βhts: s ⊆ f ⁻¹' tᶜintro.introIsBounded (f '' s)
ι: Type ?u.5624α: Type u_2β: Type u_1inst✝¹: 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 ssubset ((image_subset: ∀ {α : Type ?u.6132} {β : Type ?u.6133} {a b : Set α} (f : α → β), a ⊆ b → f '' a ⊆ f '' bimage_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 ⊆ ctrans <| image_preimage_subset: ∀ {α : Type ?u.6191} {β : Type ?u.6190} (f : α → β) (s : Set β), f '' (f ⁻¹' s) ⊆ simage_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 α) sext_iff' {t: Bornology αt t': Bornology αt' : Bornology: Type ?u.6242 → Type ?u.6242Bornology α: Type ?u.6236α} :
t: Bornology αt = t': Bornology αt' ↔ ∀ s: ?m.6252s, (@cobounded: (α : Type ?u.6255) → [inst : Bornology α] → Filter αcobounded α: Type ?u.6236α t: Bornology αt).sets: {α : Type ?u.6256} → Filter α → Set (Set α)sets s: ?m.6252s ↔ (@cobounded: (α : Type ?u.6260) → [inst : Bornology α] → Filter αcobounded α: Type ?u.6236α t': Bornology αt').sets: {α : Type ?u.6261} → Filter α → Set (Set α)sets s: ?m.6252s :=
(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 ∈ gFilter.ext_iff
#align bornology.ext_iff' Bornology.ext_iff': ∀ {α : Type u_1} {t t' : Bornology α}, t = t' ↔ ∀ (s : Set α), sets (cobounded α) s ↔ sets (cobounded α) sBornology.ext_iff'

theorem ext_iff_isBounded: ∀ {α : Type u_1} {t t' : Bornology α}, t = t' ↔ ∀ (s : Set α), IsBounded s ↔ IsBounded sext_iff_isBounded {t: Bornology αt t': Bornology αt' : Bornology: Type ?u.6312 → Type ?u.6312Bornology α: Type ?u.6303α} :
t: Bornology αt = t': Bornology αt' ↔ ∀ s: ?m.6319s, @IsBounded: {α : Type ?u.6322} → [inst : Bornology α] → Set α → PropIsBounded α: Type ?u.6303α t: Bornology αt s: ?m.6319s ↔ @IsBounded: {α : Type ?u.6324} → [inst : Bornology α] → Set α → PropIsBounded α: Type ?u.6303α t': Bornology αt' s: ?m.6319s :=
⟨fun h: ?m.6340h s: ?m.6343s => h: ?m.6340h ▸ Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl, fun h: ?m.6356h => byGoals accomplished! 🐙
ι: Type ?u.6300α: Type u_1β: Type ?u.6306t, t': Bornology αh: ∀ (s : Set α), IsBounded s ↔ IsBounded st = t'ext s: Set ?αsι: Type ?u.6300α: Type u_1β: Type ?u.6306t, t': Bornology αh: ∀ (s : Set α), IsBounded s ↔ IsBounded ss: Set αh_cobounded.as ∈ cobounded α ↔ s ∈ cobounded α
ι: Type ?u.6300α: Type u_1β: Type ?u.6306t, t': Bornology αh: ∀ (s : Set α), IsBounded s ↔ IsBounded st = 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ᶜᶜ = xcompl_compl] using h: ∀ (s : Set α), IsBounded s ↔ IsBounded sh (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 sBornology.ext_iff_isBounded

variable {s: Set αs : Set: Type ?u.6790 → Type ?u.6790Set α: 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ᶜ ∈ BisCobounded_ofBounded_iff (B: Set (Set α)B : Set: Type ?u.6641 → Type ?u.6641Set (Set: Type ?u.6642 → Type ?u.6642Set α: Type ?u.6632α)) {empty_mem: ∅ ∈ Bempty_mem subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bsubset_mem union_mem: ?m.6651union_mem sUnion_univ: ∀ (x : α), {x} ∈ BsUnion_univ} :
@IsCobounded: {α : Type ?u.6657} → [inst : Bornology α] → Set α → PropIsCobounded _: 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.6645empty_mem subset_mem: ?m.6648subset_mem union_mem: ?m.6651union_mem sUnion_univ: ?m.6654sUnion_univ) s: Set αs ↔ s: Set αsᶜ ∈ B: Set (Set α)B :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.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ᶜ ∈ BBornology.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 ∈ BisBounded_ofBounded_iff (B: Set (Set α)B : Set: Type ?u.6793 → Type ?u.6793Set (Set: Type ?u.6794 → Type ?u.6794Set α: Type ?u.6784α)) {empty_mem: ∅ ∈ Bempty_mem subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bsubset_mem union_mem: ?m.6803union_mem sUnion_univ: ∀ (x : α), {x} ∈ BsUnion_univ} :
@IsBounded: {α : Type ?u.6809} → [inst : Bornology α] → Set α → PropIsBounded _: 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.6797empty_mem subset_mem: ?m.6800subset_mem union_mem: ?m.6803union_mem sUnion_univ: ?m.6806sUnion_univ) s: Set αs ↔ s: Set αs ∈ B: Set (Set α)B := byGoals accomplished! 🐙
ι: Type ?u.6781α: Type u_1β: Type ?u.6787s: Set αB: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (x : α), {x} ∈ BIsBounded s ↔ s ∈ Brw [ι: Type ?u.6781α: Type u_1β: Type ?u.6787s: Set αB: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (x : α), {x} ∈ BIsBounded 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: ∅ ∈ Bempty_mem subset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bsubset_mem union_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ Bunion_mem sUnion_univ: ∀ (x : α), {x} ∈ BsUnion_univ),ι: Type ?u.6781α: Type u_1β: Type ?u.6787s: Set αB: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (x : α), {x} ∈ Bsᶜ ∈ cobounded α ↔ s ∈ B ι: Type ?u.6781α: Type u_1β: Type ?u.6787s: Set αB: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (x : α), {x} ∈ BIsBounded s ↔ s ∈ B← Filter.mem_sets: ∀ {α : Type ?u.6914} {f : Filter α} {s : Set α}, s ∈ f.sets ↔ s ∈ fFilter.mem_sets,ι: Type ?u.6781α: Type u_1β: Type ?u.6787s: Set αB: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (x : α), {x} ∈ Bsᶜ ∈ (cobounded α).sets ↔ s ∈ B
ι: Type ?u.6781α: Type u_1β: Type ?u.6787s: Set αB: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (x : α), {x} ∈ BIsBounded 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.6787s: Set αB: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (x : α), {x} ∈ Bsᶜ ∈ { s | sᶜ ∈ B } ↔ s ∈ B ι: Type ?u.6781α: Type u_1β: Type ?u.6787s: Set αB: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (x : α), {x} ∈ BIsBounded s ↔ s ∈ BSet.mem_setOf_eq: ∀ {α : Type ?u.6994} {x : α} {p : α → Prop}, (x ∈ { y | p y }) = p xSet.mem_setOf_eq,ι: Type ?u.6781α: Type u_1β: Type ?u.6787s: Set αB: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (x : α), {x} ∈ Bsᶜᶜ ∈ B ↔ s ∈ B ι: Type ?u.6781α: Type u_1β: Type ?u.6787s: Set αB: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (x : α), {x} ∈ BIsBounded s ↔ s ∈ Bcompl_compl: ∀ {α : Type ?u.7009} [inst : BooleanAlgebra α] (x : α), xᶜᶜ = xcompl_complι: Type ?u.6781α: Type u_1β: Type ?u.6787s: Set αB: Set (Set α)empty_mem: ∅ ∈ Bsubset_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ⊆ s₁ → s₂ ∈ Bunion_mem: ∀ (s₁ : Set α), s₁ ∈ B → ∀ (s₂ : Set α), s₂ ∈ B → s₁ ∪ s₂ ∈ BsUnion_univ: ∀ (x : α), {x} ∈ Bs ∈ 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 ∈ BBornology.isBounded_ofBounded_iff

variable [Bornology: Type ?u.7539 → Type ?u.7539Bornology α: 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.7117Set ι: Type ?u.7102ι} {f: ι → Set αf : ι: Type ?u.7102ι → Set: Type ?u.7122 → Type ?u.7122Set α: Type ?u.7105α} (hs: Set.Finite shs : s: Set ιs.Finite: {α : Type ?u.7126} → Set α → PropFinite) :
IsCobounded: {α : Type ?u.7133} → [inst : Bornology α] → Set α → PropIsCobounded (⋂ i: ?m.7143i ∈ s: Set ιs, f: ι → Set αf i: ?m.7143i) ↔ ∀ i: ?m.7201i ∈ s: Set ιs, IsCobounded: {α : Type ?u.7236} → [inst : Bornology α] → Set α → PropIsCobounded (f: ι → Set αf i: ?m.7201i) :=
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 shs
#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.7324Finset ι: Type ?u.7309ι) {f: ι → Set αf : ι: Type ?u.7309ι → Set: Type ?u.7329 → Type ?u.7329Set α: Type ?u.7312α} :
IsCobounded: {α : Type ?u.7333} → [inst : Bornology α] → Set α → PropIsCobounded (⋂ i: ?m.7343i ∈ s: Finset ιs, f: ι → Set αf i: ?m.7343i) ↔ ∀ i: ?m.7401i ∈ s: Finset ιs, IsCobounded: {α : Type ?u.7435} → [inst : Bornology α] → Set α → PropIsCobounded (f: ι → Set αf i: ?m.7401i) :=
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 ∈ fbiInter_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 → PropFinite ι: Type ?u.7527ι] {f: ι → Set αf : ι: Type ?u.7527ι → Set: Type ?u.7547 → Type ?u.7547Set α: Type ?u.7530α} :
IsCobounded: {α : Type ?u.7551} → [inst : Bornology α] → Set α → PropIsCobounded (⋂ i: ?m.7561i, f: ι → Set αf i: ?m.7561i) ↔ ∀ i: ?m.7574i, IsCobounded: {α : Type ?u.7577} → [inst : Bornology α] → Set α → PropIsCobounded (f: ι → Set αf i: ?m.7574i) :=
iInter_mem: ∀ {α : Type ?u.7591} {f : Filter α} {β : Type ?u.7590} {s : β → Set α} [inst : Finite β],
(iInter fun i => s i) ∈ f ↔ ∀ (i : β), s i ∈ fiInter_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.7739Set (Set: Type ?u.7740 → Type ?u.7740Set α: Type ?u.7727α)} (hs: Set.Finite Shs : S: Set (Set α)S.Finite: {α : Type ?u.7743} → Set α → PropFinite) :
IsCobounded: {α : Type ?u.7750} → [inst : Bornology α] → Set α → PropIsCobounded (⋂₀ S: Set (Set α)S) ↔ ∀ s: ?m.7764s ∈ S: Set (Set α)S, IsCobounded: {α : Type ?u.7802} → [inst : Bornology α] → Set α → PropIsCobounded s: ?m.7764s :=
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 Shs
#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.7860Set ι: Type ?u.7845ι} {f: ι → Set αf : ι: Type ?u.7845ι → Set: Type ?u.7865 → Type ?u.7865Set α: Type ?u.7848α} (hs: Set.Finite shs : s: Set ιs.Finite: {α : Type ?u.7869} → Set α → PropFinite) :
IsBounded: {α : Type ?u.7876} → [inst : Bornology α] → Set α → PropIsBounded (⋃ i: ?m.7886i ∈ s: Set ιs, f: ι → Set αf i: ?m.7886i) ↔ ∀ i: ?m.7944i ∈ s: Set ιs, IsBounded: {α : Type ?u.7979} → [inst : Bornology α] → Set α → PropIsBounded (f: ι → Set αf i: ?m.7944i) := byGoals accomplished! 🐙
ι: Type u_1α: Type u_2β: Type ?u.7851s✝: Set αinst✝: Bornology αs: Set ιf: ι → Set αhs: Set.Finite sIsBounded (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 sisCobounded_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 shs]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.8600Finset ι: Type ?u.8585ι) {f: ι → Set αf : ι: Type ?u.8585ι → Set: Type ?u.8605 → Type ?u.8605Set α: Type ?u.8588α} :
IsBounded: {α : Type ?u.8609} → [inst : Bornology α] → Set α → PropIsBounded (⋃ i: ?m.8619i ∈ s: Finset ιs, f: ι → Set αf i: ?m.8619i) ↔ ∀ i: ?m.8677i ∈ s: Finset ιs, IsBounded: {α : Type ?u.8711} → [inst : Bornology α] → Set α → PropIsBounded (f: ι → Set αf i: ?m.8677i) :=
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 ↑sfinite_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.8812Set (Set: Type ?u.8813 → Type ?u.8813Set α: Type ?u.8800α)} (hs: Set.Finite Shs : S: Set (Set α)S.Finite: {α : Type ?u.8816} → Set α → PropFinite) :
IsBounded: {α : Type ?u.8823} → [inst : Bornology α] → Set α → PropIsBounded (⋃₀ S: Set (Set α)S) ↔ ∀ s: ?m.8837s ∈ S: Set (Set α)S, IsBounded: {α : Type ?u.8875} → [inst : Bornology α] → Set α → PropIsBounded s: ?m.8837s := byGoals accomplished! 🐙 ι: Type ?u.8797α: Type u_1β: Type ?u.8803s: Set αinst✝: Bornology αS: Set (Set α)hs: Set.Finite SIsBounded (⋃₀ S) ↔ ∀ (s : Set α), s ∈ S → IsBounded srw [ι: Type ?u.8797α: Type u_1β: Type ?u.8803s: Set αinst✝: Bornology αS: Set (Set α)hs: Set.Finite SIsBounded (⋃₀ S) ↔ ∀ (s : Set α), s ∈ S → IsBounded ssUnion_eq_biUnion: ∀ {α : Type ?u.8889} {s : Set (Set α)}, ⋃₀ s = iUnion fun i => iUnion fun _h => isUnion_eq_biUnion,ι: Type ?u.8797α: Type u_1β: Type ?u.8803s: Set αinst✝: Bornology αS: Set (Set α)hs: Set.Finite SIsBounded (iUnion fun i => iUnion fun _h => i) ↔ ∀ (s : Set α), s ∈ S → IsBounded s ι: Type ?u.8797α: Type u_1β: Type ?u.8803s: Set αinst✝: Bornology αS: Set (Set α)hs: Set.Finite SIsBounded (⋃₀ 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 Shsι: Type ?u.8797α: Type u_1β: Type ?u.8803s: 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 → PropFinite ι: Type ?u.8975ι] {s: ι → Set αs : ι: Type ?u.8975ι → Set: Type ?u.8995 → Type ?u.8995Set α: Type ?u.8978α} : IsBounded: {α : Type ?u.8999} → [inst : Bornology α] → Set α → PropIsBounded (⋃ i: ?m.9009i, s: ι → Set αs i: ?m.9009i) ↔ ∀ i: ?m.9022i, IsBounded: {α : Type ?u.9025} → [inst : Bornology α] → Set α → PropIsBounded (s: ι → Set αs i: ?m.9022i) :=
byGoals accomplished! 🐙 ι: Type u_1α: Type u_2β: Type ?u.8981s✝: 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.8981s✝: 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 xsUnion_range,ι: Type u_1α: Type u_2β: Type ?u.8981s✝: 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.8981s✝: 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.8981s✝: 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.8981s✝: 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.8981s✝: 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 sSet.Finite.isBounded [Bornology: Type ?u.9197 → Type ?u.9197Bornology α: Type ?u.9191α] {s: Set αs : Set: Type ?u.9200 → Type ?u.9200Set α: Type ?u.9191α} (hs: Set.Finite shs : s: Set αs.Finite: {α : Type ?u.9203} → Set α → PropFinite) : IsBounded: {α : Type ?u.9210} → [inst : Bornology α] → Set α → PropIsBounded s: Set αs :=
Bornology.le_cofinite: ∀ (α : Type ?u.9227) [inst : Bornology α], cobounded α ≤ cofiniteBornology.le_cofinite α: Type ?u.9191α hs: Set.Finite shs.compl_mem_cofinite: ∀ {α : Type ?u.9238} {s : Set α}, Set.Finite s → sᶜ ∈ cofinitecompl_mem_cofinite
#align set.finite.is_bounded Set.Finite.isBounded: ∀ {α : Type u_1} [inst : Bornology α] {s : Set α}, Set.Finite s → IsBounded sSet.Finite.isBounded

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

/-- The cofinite filter as a bornology -/
@[reducible]
def Bornology.cofinite: Bornology αBornology.cofinite : Bornology: Type ?u.9865 → Type ?u.9865Bornology α: Type ?u.9859α
where
cobounded' := Filter.cofinite: {α : Type ?u.9870} → Filter αFilter.cofinite
le_cofinite' := le_rfl: ∀ {α : Type ?u.9873} [inst : Preorder α] {a : α}, a ≤ ale_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.10024Bornology α: Type ?u.10021α] : Prop: TypeProp where
/-- The `Set.univ` is bounded. -/
bounded_univ: ∀ {α : Type u_1} [inst : Bornology α] [self : BoundedSpace α], IsBounded univbounded_univ : Bornology.IsBounded: {α : Type ?u.10028} → [inst : Bornology α] → Set α → PropBornology.IsBounded (univ: {α : Type ?u.10036} → Set αuniv : Set: Type ?u.10035 → Type ?u.10035Set α: Type ?u.10021α)
#align bounded_space BoundedSpace: (α : Type u_1) → [inst : Bornology α] → PropBoundedSpace

namespace Bornology

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

theorem isBounded_univ: ∀ {α : Type u_1} [inst : Bornology α], IsBounded univ ↔ BoundedSpace αisBounded_univ : IsBounded: {α : Type ?u.10078} → [inst : Bornology α] → Set α → PropIsBounded (univ: {α : Type ?u.10083} → Set αuniv : Set: Type ?u.10082 → Type ?u.10082Set α: Type ?u.10069α) ↔ BoundedSpace: (α : Type ?u.10090) → [inst : Bornology α] → PropBoundedSpace α: Type ?u.10069α :=
⟨fun h: ?m.10102h => ⟨h: ?m.10102h⟩, fun h: ?m.10125h => h: ?m.10125h.1: ∀ {α : Type ?u.10127} [inst : Bornology α] [self : BoundedSpace α], IsBounded univ1⟩
#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 α] → PropBoundedSpace α: Type ?u.10141α := byGoals accomplished! 🐙
ι: Type ?u.10138α: Type u_1β: Type ?u.10144inst✝: Bornology αcobounded α = ⊥ ↔ BoundedSpace αrw [ι: Type ?u.10138α: Type u_1β: Type ?u.10144inst✝: Bornology αcobounded α = ⊥ ↔ BoundedSpace α← isBounded_univ: ∀ {α : Type ?u.10242} [inst : Bornology α], IsBounded univ ↔ BoundedSpace αisBounded_univ,ι: Type ?u.10138α: Type u_1β: Type ?u.10144inst✝: Bornology αcobounded α = ⊥ ↔ IsBounded univ ι: Type ?u.10138α: Type u_1β: Type ?u.10144inst✝: 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.10144inst✝: Bornology αcobounded α = ⊥ ↔ univᶜ ∈ cobounded α ι: Type ?u.10138α: Type u_1β: Type ?u.10144inst✝: Bornology αcobounded α = ⊥ ↔ BoundedSpace αcompl_univ: ∀ {α : Type ?u.10274}, univᶜ = ∅compl_univ,ι: Type ?u.10138α: Type u_1β: Type ?u.10144inst✝: Bornology αcobounded α = ⊥ ↔ ∅ ∈ cobounded α ι: Type ?u.10138α: Type u_1β: Type ?u.10144inst✝: 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.10144inst✝: 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 α] → PropBoundedSpace α: Type ?u.10318α]

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

theorem IsCobounded.all: ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : BoundedSpace α] (s : Set α), IsCobounded sIsCobounded.all (s: Set αs : Set: Type ?u.10446 → Type ?u.10446Set α: Type ?u.10430α) : IsCobounded: {α : Type ?u.10449} → [inst : Bornology α] → Set α → PropIsCobounded s: Set αs :=
compl_compl: ∀ {α : Type ?u.10464} [inst : BooleanAlgebra α] (x : α), xᶜᶜ = xcompl_compl s: Set αs ▸ IsBounded.all: ∀ {α : Type ?u.10475} [inst : Bornology α] [inst_1 : BoundedSpace α] (s : Set α), IsBounded sIsBounded.all (s: Set αsᶜ)
#align bornology.is_cobounded.all Bornology.IsCobounded.all: ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : BoundedSpace α] (s : Set α), IsCobounded sBornology.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 → a2 ‹_›
#align bornology.cobounded_eq_bot Bornology.cobounded_eq_bot: ∀ (α : Type u_1) [inst : Bornology α] [inst_1 : BoundedSpace α], cobounded α = ⊥Bornology.cobounded_eq_bot

end Bornology
```