encode_lt_comp — Mathlib

English

For cf,cg, encoding cf and cg are less than encoding of comp cf cg.

Русский

Для cf,cg код cf и cg меньше кодирования comp cf cg.

LaTeX

$$$\\operatorname{encodeCode}(cf) < \\operatorname{encodeCode}(\\mathrm{comp}(cf,cg)) \\land \\operatorname{encodeCode}(cg) < \\operatorname{encodeCode}(\\mathrm{comp}(cf,cg))$$$

Lean4

theorem encode_lt_comp (cf cg) : encode cf < encode (comp cf cg) ∧ encode cg < encode (comp cf cg) :=
  by
  have : encode (pair cf cg) < encode (comp cf cg) := by simp [encodeCode_eq, encodeCode]
  exact (encode_lt_pair cf cg).imp (fun h => lt_trans h this) fun h => lt_trans h this

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