mono_on — Mathlib

English

If s has PairwiseDisjoint f and g i ≤ f i for all i in s, then s has PairwiseDisjoint g.

Русский

Если s попарно непересекается по f и g(i) ≤ f(i) для всех i∈s, то s попарно непересекается по g.

LaTeX

$$hs : s.PairwiseDisjoint f \\Rightarrow (∀ ⦃i⦄, i ∈ s → g i ≤ f i) → s.PairwiseDisjoint g$$

Lean4

theorem mono_on (hs : s.PairwiseDisjoint f) (h : ∀ ⦃i⦄, i ∈ s → g i ≤ f i) : s.PairwiseDisjoint g :=
  fun _a ha _b hb hab => (hs ha hb hab).mono (h ha) (h hb)

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