diam_iUnion_mem_option — Mathlib

English

The diameter of the union over an optional index equals the supremum of the diameters of the pieces.

Русский

Диаметр объединения по опциональному индексу равен инфимуму-супремуму диаметров составляющих.

LaTeX

$$\operatorname{diam}\left(\bigcup i \in o, s(i)\right) = \bigvee_{i \in o} \operatorname{diam}(s(i))$$

Lean4

theorem diam_iUnion_mem_option {ι : Type*} (o : Option ι) (s : ι → Set α) : diam (⋃ i ∈ o, s i) = ⨆ i ∈ o, diam (s i) :=
  by cases o <;> simp

Похожие утверждения