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.
/-
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'
:=

Goals accomplished! 🐙
ι: Type ?u.289

α: Type u_1

β: Type ?u.295

t, t': Bornology α

h_cobounded: cobounded α = cobounded α


t = 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'
ι: 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'

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 :=

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 }
ι: 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 }
ι: 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 }

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
=>

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 }

Goals accomplished! 🐙
} le_cofinite' :=

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 }) } ≤ cofinite
ι: 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 }) } ≤ cofinite
ι: 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 }) } ≤ cofinite
ι: 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 }) } ≤ cofinite
ι: 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: α


ι: 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 }) } ≤ cofinite
ι: 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: α


ι: 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 }) } ≤ cofinite

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
=>

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} ∈ 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} ∈ 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
ι: 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
ι: 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} ∈ 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: α

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} ∈ B

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
:=

Goals accomplished! 🐙
ι: Type ?u.3987

α: Type u_1

β: Type ?u.3993

inst✝: Bornology α

s, t: Set α

x: α


ι: Type ?u.3987

α: Type u_1

β: Type ?u.3993

inst✝: Bornology α

s, t: Set α

x: α


ι: Type ?u.3987

α: Type u_1

β: Type ?u.3993

inst✝: Bornology α

s, t: Set α

x: α


ι: Type ?u.3987

α: Type u_1

β: Type ?u.3993

inst✝: Bornology α

s, t: Set α

x: α


ι: Type ?u.3987

α: Type u_1

β: Type ?u.3993

inst✝: Bornology α

s, t: Set α

x: α


ι: Type ?u.3987

α: Type u_1

β: Type ?u.3993

inst✝: Bornology α

s, t: Set α

x: α


ι: Type ?u.3987

α: Type u_1

β: Type ?u.3993

inst✝: Bornology α

s, t: Set α

x: α



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
α
) :=

Goals accomplished! 🐙
ι: Type ?u.4271

α: Type u_1

β: Type ?u.4277

inst✝: Bornology α

s, t: Set α

x: α


ι: Type ?u.4271

α: Type u_1

β: Type ?u.4277

inst✝: Bornology α

s, t: Set α

x: α


ι: Type ?u.4271

α: Type u_1

β: Type ?u.4277

inst✝: Bornology α

s, t: Set α

x: α


ι: Type ?u.4271

α: Type u_1

β: Type ?u.4277

inst✝: Bornology α

s, t: Set α

x: α


ι: 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: α



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
α
) :=

Goals accomplished! 🐙
ι: Type ?u.4415

α: Type u_1

β: Type ?u.4421

inst✝: Bornology α

s, t: Set α

x: α


ι: Type ?u.4415

α: Type u_1

β: Type ?u.4421

inst✝: Bornology α

s, t: Set α

x: α


ι: Type ?u.4415

α: Type u_1

β: Type ?u.4421

inst✝: Bornology α

s, t: Set α

x: α


ι: Type ?u.4415

α: Type u_1

β: Type ?u.4421

inst✝: Bornology α

s, t: Set α

x: α


ι: Type ?u.4415

α: Type u_1

β: Type ?u.4421

inst✝: Bornology α

s, t: Set α

x: α



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: {α : Type ?u.4738} → [inst : Bornology α] → Set α → Prop
IsCobounded
s: Set α
s
) (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, 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
:=

Goals accomplished! 🐙
ι: Type ?u.4828

α: Type u_1

β: Type ?u.4834

inst✝: Bornology α

s, t: Set α

x: α



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: {α : 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
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
) :=

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)
ι: 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


ι: 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)
ι: 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.intro
ι: 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)
ι: 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.intro
ι: 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.intro
ι: 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.intro
ι: 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.intro
ι: 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.intro
ι: 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.intro
ι: 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)

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
=>

Goals accomplished! 🐙
ι: Type ?u.6300

α: Type u_1

β: Type ?u.6306

t, t': Bornology α

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


t = t'
ι: Type ?u.6300

α: Type u_1

β: Type ?u.6306

t, t': Bornology α

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

s: Set α


h_cobounded.a
ι: Type ?u.6300

α: Type u_1

β: Type ?u.6306

t, t': Bornology α

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


t = t'

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
:=

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


ι: 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


ι: 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


ι: 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


ι: 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


ι: 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


ι: 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


ι: 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


ι: 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


ι: 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


ι: 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



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 :
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 #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 :
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 #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 :
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
) :=

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)

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 :
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
:=

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 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 s
ι: 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 s
ι: 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
) :=

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)
ι: 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)
ι: 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)
ι: 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)
ι: 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 :
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.
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
α
:=

Goals accomplished! 🐙
ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α


ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α


ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α


ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α


ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α


ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α


ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α


ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α


ι: Type ?u.10138

α: Type u_1

β: Type ?u.10144

inst✝: Bornology α



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