powerset_mono — Mathlib

English

Powerset is monotone: s ⊆ t if and only if powerset(s) ⊆ powerset(t).

Русский

Множество подмножеств монотонно: s ⊆ t тогда и только тогда, когда powerset(s) ⊆ powerset(t).

LaTeX

$$$$\\text{powerset } s \\subseteq \\text{powerset } t \\;\\iff\\; s \\subseteq t.$$$$

Lean4

@[simp]
theorem powerset_mono {s t : Finset α} : powerset s ⊆ powerset t ↔ s ⊆ t :=
  ⟨fun h => mem_powerset.1 <| h <| mem_powerset_self _, fun st _u h =>
    mem_powerset.2 <| Subset.trans (mem_powerset.1 h) st⟩

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