domain_mono — Mathlib

English

The map that assigns to each partial linear map its domain is strictly monotone: if f < g then dom(f) < dom(g).

Русский

Отображение, которое ставит в соответствие частичному линейному отображению его область определения, строго монотонно: если f < g, то dom(f) < dom(g).

LaTeX

$$$\\text{domain}: (f,g) \\mapsto \\operatorname{dom}(f)\\,$ is strictly monotone: if $f

Lean4

theorem domain_mono : StrictMono (@domain R _ E _ _ F _ _) := fun _f _g hlt =>
  lt_of_le_of_ne hlt.1.1 fun heq => ne_of_lt hlt <| eq_of_le_of_domain_eq (le_of_lt hlt) heq

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