English
Given a family B of bounded sets closed under subsets and unions, with empty and singletons in B, one obtains a Bornology whose cobounded sets are generated by B.
Русский
Дано семейство B ограниченных множеств, замкнутое по подмножествам и объединениям, содержащее пустое множество и одиночку; существует борология с кобBounded, порождаемой B.
LaTeX
$$$B \\subseteq \\mathcal P(\\alpha),\\ ∅ \\in B,\\ s_1 \\in B,\\ s_2 \\subseteq s_1 \\Rightarrow s_2 \\in B,\\ s_1, s_2 \\in B \\Rightarrow s_1 \\cup s_2 \\in B,\\ \\forall x,\\ {x} \\in B \\Rightarrow \\text{Bornology }\\alpha \\text{ exists with } \\text{cobounded } = \\mathrm{comk}(s \\in B)$$$
Lean4
/-- A constructor for bornologies by specifying the bounded sets,
and showing that they satisfy the appropriate conditions. -/
@[simps]
def ofBounded {α : Type*} (B : Set (Set α)) (empty_mem : ∅ ∈ B) (subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B)
(union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B) (singleton_mem : ∀ x, { x } ∈ B) : Bornology α
where
cobounded := comk (· ∈ B) empty_mem subset_mem union_mem
le_cofinite := by simpa [le_cofinite_iff_compl_singleton_mem]
