compls_subset_iff — Mathlib

English

Let α be a Boolean algebra and s,t finite subsets of α. The complement of s, denoted sᶜˢ, satisfies sᶜˢ ⊆ t if and only if s ⊆ tᶜˢ.

Русский

Пусть α — булова алгебра, а s,t — конечные подмножества α. Комплемент s, обозначаемый sᶜˢ, удовлетворяет sᶜˢ ⊆ t тогда и только тогда, когда s ⊆ tᶜˢ.

LaTeX

$$$s^{\!c_s} \subseteq t \iff s \subseteq t^{\!c_s}$$$

Lean4

theorem compls_subset_iff : sᶜˢ ⊆ t ↔ s ⊆ tᶜˢ := by rw [← compls_subset_compls, compls_compls]

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