Set_Complement_inverts_Subsets
Provedproofwikiset-complementsubsets
S is a subset of T if and only if the complement of T is a subset of the complement of S.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Set_Complement_inverts_Subsets {alpha : Type _} (S T : Set alpha) :
S <= T <-> T.compl <= S.compl := by sorrySource