congr — Mathlib

English

If f1 and f2 are equal on s, then the strict monotonicity on s of f1 is equivalent to that of f2.

Русский

Если f1 и f2 совпадают на s, то строгая мономорность на s f1 эквивалентна строгой мономорности на s f2.

LaTeX

$$$\\forall {\\alpha \\beta},\\ s: Set\\alpha,\\ f_1,f_2: \\alpha \\to \\beta,\\ [Preorder\\alpha][Preorder\\beta]\\n( h_1 : \\operatorname{StrictMonoOn} f_1 s ) \\to ( s.EqOn f_1 f_2 s ) \\to \\operatorname{StrictMonoOn} f_2 s$$$

Lean4

theorem _root_.StrictMonoOn.congr (h₁ : StrictMonoOn f₁ s) (h : s.EqOn f₁ f₂) : StrictMonoOn f₂ s :=
  by
  intro a ha b hb hab
  rw [← h ha, ← h hb]
  exact h₁ ha hb hab

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