English
Variant construction of a Bornology using a family B with a specified universal union.
Русский
Вариант конструктора борологии с использованием семейства B, имеющего объединение равное вселенной.
LaTeX
$$$B, empty, subset, union, sUnion = univ \\Rightarrow \\text{Bornology }\\alpha \\text{ with } cobounded = comk( B )$$$
Lean4
/-- A constructor for bornologies by specifying the bounded sets,
and showing that they satisfy the appropriate conditions. -/
@[simps! cobounded]
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) (sUnion_univ : ⋃₀ B = univ) : Bornology α :=
Bornology.ofBounded B empty_mem subset_mem union_mem fun x =>
by
rw [sUnion_eq_univ_iff] at sUnion_univ
rcases sUnion_univ x with ⟨s, hs, hxs⟩
exact subset_mem s hs { x } (singleton_subset_iff.mpr hxs)
