union — Mathlib

English

If s and t are inaccessible by directed joins, then s ∪ t is inaccessible by directed joins.

Русский

Если s и t недоступны по направленным объединениям, то их объединение недоступно по направленным объединениям.

LaTeX

$$$\\forall s,t,\\ \\text{DirSupInacc}(s)\\to \\text{DirSupInacc}(t)\\to \\text{DirSupInacc}(s\\cup t)$$$

Lean4

theorem union (hs : DirSupInacc s) (ht : DirSupInacc t) : DirSupInacc (s ∪ t) := by
  rw [← dirSupClosed_compl, compl_union]; exact hs.compl.inter ht.compl

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