Theorems · Inductive type · order theory

ContravariantClass

(M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop

Given an action μ of a Type M on a Type N and a relation r on N, informally, the ContravariantClass says that "if the result of the action μ on a pair satisfies the relation r, then the initial pair satisfied the relation r." More precisely, the ContravariantClass is a class taking two Types M N, together with an "action" μ : M → N → N and a relation r : N → N → Prop. Its unique field elim is the assertion that for all m ∈ M and all elements n₁, n₂ ∈ N, if the relation r holds for the pair (μ m n₁, μ m n₂) obtained from (n₁, n₂) by acting upon it by m, then, the relation r also holds for the pair (n₁, n₂). If m : M and h : r (μ m n₁) (μ m n₂), then ContravariantClass.elim m h : r n₁ n₂.

Defined in

Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Cited by

15 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms