dirSupInacc_compl — Mathlib

English

The complement of a set s is DirSupInacc iff s is DirSupClosed.

Русский

Комплемент множества s является DirSupInacc тогда и только тогда, когда s является DirSupClosed.

LaTeX

$$$\\text{DirSupClosed}(s) \\iff \\text{DirSupInacc}(s^{\\complement})$$$

Lean4

@[simp]
theorem dirSupInacc_compl : DirSupInacc sᶜ ↔ DirSupClosed s := by
  simp [DirSupInacc, DirSupClosed, ← not_disjoint_iff_nonempty_inter, not_imp_not, disjoint_compl_right_iff]

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