mono — Mathlib

English

Codisjoint is monotone in both arguments: if a ≤ b and c ≤ d and a codisjoint with c, then b is codisjoint with d.

Русский

Кодиссоединение монотонно по обеим аргументам: если a ≤ b и c ≤ d, и a кодиссоединено с c, то b кодиссоединено с d.

LaTeX

$$$(a \le b) \to (c \le d) \to \operatorname{Codisjoint}(a,c) \to \operatorname{Codisjoint}(b,d)$$$

Lean4

@[gcongr]
theorem mono (h₁ : a ≤ b) (h₂ : c ≤ d) : Codisjoint a c → Codisjoint b d := fun h _ ha hc ↦
  h (h₁.trans ha) (h₂.trans hc)

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