sup_join — Mathlib

English

The join of two filters’ joins equals the join of the joins: join f1 ⊔ join f2 = join (f1 ⊔ f2).

Русский

Объединение двух фильтровных объединений равняется объединению их объединений: join f1 ⊔ join f2 = join (f1 ⊔ f2).

LaTeX

$$join f1 ⊔ join f2 = join (f1 ⊔ f2)$$

Lean4

@[simp]
theorem sup_join {f₁ f₂ : Filter (Filter α)} : join f₁ ⊔ join f₂ = join (f₁ ⊔ f₂) :=
  Filter.ext fun x => by simp only [mem_sup, mem_join]

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