Anti-additivity

[zwarts-1998] [icard-2012]

The Zwarts function classes the polarity literature quantifies over: IsAntiAdditive (f (p ⊔ q) = f p ⊓ f q), IsAntiMultiplicative (meets to joins), and IsAntiMorphic (both) — the semantic content of the DE strength hierarchy (Polarity.DEStrength.HoldsFor) and of the anti- signature rows (Signature.Property.HoldsFor in Soundness.lean). Each implies antitonicity, and complementation realizes the full anti-morphism. The dual UE-side properties (preserving joins or meets) have no named classes — consumers state the equations directly, with monotone_of_map_sup and monotone_of_map_inf supplying monotonicity.

The anti- classes

def NaturalLogic.IsAntiAdditive {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeInf β] (f : α → β) : Prop

Anti-additive: f (p ⊔ q) = f p ⊓ f q, polymorphic in domain and codomain.

Equations

• NaturalLogic.IsAntiAdditive f = ∀ (p q : α), f (p ⊔ q) = f p ⊓ f q

def NaturalLogic.IsAntiMultiplicative {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeSup β] (f : α → β) : Prop

Anti-multiplicative: f (p ⊓ q) = f p ⊔ f q.

Equations

• NaturalLogic.IsAntiMultiplicative f = ∀ (p q : α), f (p ⊓ q) = f p ⊔ f q

def NaturalLogic.IsAntiMorphic {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : α → β) : Prop

Anti-morphic: anti-additive and anti-multiplicative.

Equations

• NaturalLogic.IsAntiMorphic f = (NaturalLogic.IsAntiAdditive f ∧ NaturalLogic.IsAntiMultiplicative f)

theorem NaturalLogic.monotone_of_map_sup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : ∀ (p q : α), f (p ⊔ q) = f p ⊔ f q) : Monotone f

A join-preserving function is monotone.

theorem NaturalLogic.monotone_of_map_inf {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (h : ∀ (p q : α), f (p ⊓ q) = f p ⊓ f q) : Monotone f

A meet-preserving function is monotone.

theorem NaturalLogic.IsAntiAdditive.antitone {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeInf β] {f : α → β} (h : IsAntiAdditive f) : Antitone f

Anti-additive implies antitone.

theorem NaturalLogic.IsAntiMultiplicative.antitone {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeSup β] {f : α → β} (h : IsAntiMultiplicative f) : Antitone f

Anti-multiplicative implies antitone.

theorem NaturalLogic.IsAntiMorphic.antiAdditive {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] {f : α → β} (h : IsAntiMorphic f) : IsAntiAdditive f

Anti-morphic implies anti-additive.

theorem NaturalLogic.IsAntiMorphic.antiMultiplicative {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] {f : α → β} (h : IsAntiMorphic f) : IsAntiMultiplicative f

Anti-morphic implies anti-multiplicative.

theorem NaturalLogic.IsAntiMorphic.antitone {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] {f : α → β} (h : IsAntiMorphic f) : Antitone f

Anti-morphic implies antitone.

Complementation

theorem NaturalLogic.isAntiAdditive_compl {α : Type u_1} [BooleanAlgebra α] : IsAntiAdditive compl

theorem NaturalLogic.isAntiMultiplicative_compl {α : Type u_1} [BooleanAlgebra α] : IsAntiMultiplicative compl

theorem NaturalLogic.isAntiMorphic_compl {α : Type u_1} [BooleanAlgebra α] : IsAntiMorphic compl

theorem NaturalLogic.antitone_compl {α : Type u_1} [BooleanAlgebra α] : Antitone compl

Pointwise bridges

The anti-additivity equation at the Set- and Prop-valued instances, in the membership forms consumers destructure.

theorem NaturalLogic.isAntiAdditive_iff_mem {γ : Type u_1} {δ : Type u_2} {f : Set γ → Set δ} : IsAntiAdditive f ↔ ∀ (p q : Set γ) (x : δ), x ∈ f (p ∪ q) ↔ x ∈ f p ∧ x ∈ f q

theorem NaturalLogic.isAntiAdditive_iff_gq {γ : Type u_1} {f : Set γ → Prop} : IsAntiAdditive f ↔ ∀ (p q : Set γ), f (p ∪ q) ↔ f p ∧ f q

The Prop-valued instance: anti-additivity is f (p ∪ q) ↔ f p ∧ f q.

theorem NaturalLogic.isAntiAdditive_forall_mem {α : Type u_3} {β : Type u_4} (P : α → β → Prop) : IsAntiAdditive fun (X : Set α) (y : β) => ∀ (x : α), x ∈ X → P x y

Any function of the form fun X y => ∀ x ∈ X, P x y is anti-additive in X.