rel_mono — Mathlib

English

If s is bounded with respect to r and r ≤ r', then s is bounded with respect to r'.

Русский

Если множество s ограничено относительно отношения r и r ≤ r', то оно ограничено относительно r'.

LaTeX

$$$ \operatorname{Bounded}(r,s) \land (r \le r') \Rightarrow \operatorname{Bounded}(r',s) $$$

Lean4

theorem rel_mono {r' : α → α → Prop} (h : Bounded r s) (hrr' : r ≤ r') : Bounded r' s :=
  let ⟨a, ha⟩ := h
  ⟨a, fun b hb => hrr' b a (ha b hb)⟩

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