Theorems · Inductive type · order theory

CovariantClass

(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 CovariantClass says that "the action μ preserves the relation r." More precisely, the CovariantClass 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 (n₁, n₂), then, the relation r also holds for the pair (μ m n₁, μ m n₂), obtained from (n₁, n₂) by acting upon it by m. If m : M and h : r n₁ n₂, then CovariantClass.elim m h : r (μ m n₁) (μ m n₂).

Defined in

Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Cited by

25 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms