einfsep_iUnion_mem_option — Mathlib

English

The einfsep distributes over unions indexed by an option: einfsep(⋃ i ∈ o, s i) = ⨅ i ∈ o, (s i).einfsep.

Русский

Расширенная инфиминальная разделённость распадается по объединениям, индексируемым опцией: einfsep(⋃ i ∈ o, s i) = ⨅ i ∈ o, (s i).einfsep.

LaTeX

$$$\operatorname{einfsep}\big(\bigcup_{i \in o} s_i\big) = \bigwedge_{i \in o} (s_i)\einfsep$$$

Lean4

theorem einfsep_iUnion_mem_option {ι : Type*} (o : Option ι) (s : ι → Set α) :
    (⋃ i ∈ o, s i).einfsep = ⨅ i ∈ o, (s i).einfsep := by cases o <;> simp

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