powerset_sups_powerset_self — Mathlib

English

In a distributive lattice, the join of a powerset with itself is just the powerset: s.powerset ⊻ s.powerset = s.powerset.

Русский

В распределительной решётке объединение (powerset) самой множины с самой собой равно самому powerset.

LaTeX

$$$ s.powerset \vee s.powerset = s.powerset $$$

Lean4

@[simp]
theorem powerset_sups_powerset_self (s : Finset α) : s.powerset ⊻ s.powerset = s.powerset := by simp [← powerset_union]

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