mono — Mathlib

English

Alternate monotonicity lemma for MemBaseSet.

Русский

Альтернативная лемма монотонности MemBaseSet.

LaTeX

$$$l_1.MemBaseSet I c_1 r_1 \\Rightarrow l_2.MemBaseSet I c_2 r_2$ under monotone conditions$$

Lean4

@[mono]
theorem mono (h : l₁ ≤ l₂) (hc : c₁ ≤ c₂) (hr : ∀ x ∈ Box.Icc I, r₁ x ≤ r₂ x) (hπ : l₁.MemBaseSet I c₁ r₁ π) :
    l₂.MemBaseSet I c₂ r₂ π :=
  hπ.mono' I h hc fun J _ => hr _ <| π.tag_mem_Icc J

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