Disjoint complements

The disjoint complement Aᵈ of a set A ⊆ X consists of all elements of X disjoint from every member of A. It is always a band, and behaves naturally with respect to inclusion, union, and double complementation.

In a normed vector lattice, every disjoint complement is norm closed: it is an intersection of zero-sets of the continuous maps x ↦ |x| ⊓ |a|.

The disjoint complement as a set

def disjointComplement {X : Type u_1} [AddCommGroup X] [Lattice X] (A : Set X) : Set X

The disjoint complement of a set A ⊆ X is the set of all elements disjoint from every member of A.

Equations

• Aᵈ = {x : X | ∀ a ∈ A, IsVLDisjoint x a}

def «term_ᵈ» : Lean.TrailingParserDescr

The disjoint complement of a set A ⊆ X is the set of all elements disjoint from every member of A.

Equations

• «term_ᵈ» = Lean.ParserDescr.trailingNode `«term_ᵈ» 1024 1024 (Lean.ParserDescr.symbol "ᵈ")

theorem mem_disjointComplement_iff {X : Type u_1} [AddCommGroup X] [Lattice X] {A : Set X} {x : X} : x ∈ Aᵈ ↔ ∀ a ∈ A, IsVLDisjoint x a

Membership in the disjoint complement: x ∈ Aᵈ iff x is disjoint from every member of A.

theorem disjointComplement_anti {X : Type u_1} [AddCommGroup X] [Lattice X] {A B : Set X} (h : A ⊆ B) : Bᵈ ⊆ Aᵈ

Disjoint complementation is anti-monotone: A ⊆ B implies Bᵈ ⊆ Aᵈ.

theorem disjointComplement_inter_eq_zero {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (A : Set X) : A ∩ Aᵈ ⊆ {0}

The intersection of a set with its disjoint complement is contained in {0}.

theorem subset_disjointComplement_disjointComplement {X : Type u_1} [AddCommGroup X] [Lattice X] (A : Set X) : A ⊆ Aᵈᵈ

Every set is contained in its double disjoint complement.

theorem disjointComplement_disjointComplement_disjointComplement {X : Type u_1} [AddCommGroup X] [Lattice X] (A : Set X) : Aᵈᵈᵈ = Aᵈ

The triple disjoint complement equals the single disjoint complement.

theorem disjointComplement_union {X : Type u_1} [AddCommGroup X] [Lattice X] (A B : Set X) : (A ∪ B)ᵈ = Aᵈ ∩ Bᵈ

The disjoint complement of a union is the intersection of the disjoint complements.

theorem disjointComplement_union_disjointComplement_eq_singleton {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (A : Set X) : (A ∪ Aᵈ)ᵈ = {0}

The disjoint complement of a set together with its disjoint complement is the singleton {0}.

The disjoint complement is a band

def Band.disjointComplement {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (A : Set X) : Band X

The disjoint complement of any set is a band.

Equations

• Band.disjointComplement A = Band.ofPosDirectedSSupMem (OrderIdeal.ofSolid { carrier := Aᵈ, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } ⋯) ⋯

Closedness in normed vector lattices

theorem isClosed_disjointComplement {X : Type u_2} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] (A : Set X) : IsClosed Aᵈ

In a normed vector lattice, the disjoint complement of any set is norm closed: it is the intersection of the zero-sets of the continuous maps x ↦ |x| ⊓ |a|.