mono' — Mathlib

English

If hs is DirectedOn r s and whenever a,b ∈ s with r a b one has r' a b, then hs is DirectedOn r' s.

Русский

Если s направлено относительно r и если для любых a,b ∈ s при r a b выполняется r' a b, то s направлено относительно r'.

LaTeX

$$$DirectedOn\\ r\\ s \\to\\ (\\\\forall {a} {b}, a \\\\in s \\\\to b \\\\in s \\\\to r a b \\\\to r' a b) \\to DirectedOn\\ r'\\ s$$$

Lean4

theorem mono' {s : Set α} (hs : DirectedOn r s) (h : ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → r a b → r' a b) : DirectedOn r' s :=
  fun _ hx _ hy =>
  let ⟨z, hz, hxz, hyz⟩ := hs _ hx _ hy
  ⟨z, hz, h hx hz hxz, h hy hz hyz⟩

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