Theorems · Theorem · general topology

Bornology.isBounded_biUnion

∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] {s : Set ι} {f : ι → Set α},
  s.Finite → (Bornology.IsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, Bornology.IsBounded (f i))

Defined in

Mathlib.Topology.Bornology.Basic

Cited by

3 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Bornology