rel_iff_cov — Mathlib

English

For a system with a function μ and a relation r on N, if Covariant and Contravariant classes hold, then r(μ m a, μ m b) holds iff r(a,b).

Русский

Для системы с действием μ и отношением r на N, если выполняются классы Covariant и Contravariant, то r(μ m a, μ m b) эквивалентно r(a,b).

LaTeX

$$∀ (M N μ r) [CovariantClass M N μ r] [ContravariantClass M N μ r] (m : M) {a b : N}, r(μ m a, μ m b) ↔ r a b$$

Lean4

theorem rel_iff_cov [CovariantClass M N μ r] [ContravariantClass M N μ r] (m : M) {a b : N} :
    r (μ m a) (μ m b) ↔ r a b :=
  ⟨ContravariantClass.elim _, CovariantClass.elim _⟩

Похожие утверждения