extend_mono' — Mathlib

English

If P is a property of sets and m satisfies a monotonicity condition, then extend m is monotone with respect to inclusion.

Русский

Пусть P — свойство множества, а функция m удовлетворяет условию монотонности; тогда расширение m монотонно по включениям.

LaTeX

$$$\\text{If } P(s_1) \\text{ and } s_1 \\subseteq s_2, \\text{ then } \\operatorname{extend} m\\,s_1 \\le \\operatorname{extend} m\\,s_2$$$

Lean4

theorem extend_mono' ⦃s₁ s₂ : Set α⦄ (h₁ : P s₁) (hs : s₁ ⊆ s₂) : extend m s₁ ≤ extend m s₂ :=
  by
  refine le_iInf ?_
  intro h₂
  rw [extend_eq m h₁]
  exact m_mono h₁ h₂ hs

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