mk_le_mk — Mathlib

English

The pointwise-constructed simple functions satisfy the same order relations as their underlying pointwise functions: mk f hf hf' ≤ mk g hg hg' iff f ≤ g.

Русский

У конструкций mk выполняется то же неравенство, что и для соответствующих функций: mk f hf hf' ≤ mk g hg hg' если и только если f ≤ g.

LaTeX

$$$mk f hf hf' \\le mk g hg hg' \\iff f \\le g.$$$

Lean4

@[simp]
theorem mk_le_mk {f g : α → β} {hf hg hf' hg'} : mk f hf hf' ≤ mk g hg hg' ↔ f ≤ g :=
  Iff.rfl

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