mono' — Mathlib

English

Definition: the set of prepartitions containing those satisfying MemBaseSet.

Русский

Определение: множество предразбиований, содержащих те, что удовлетворяют MemBaseSet.

LaTeX

$$$\\text{toFilterDistortion}(l,I,c) := \\langle \\text{the } \\mathcal{P}\\{\\pi : l.MemBaseSet I c r \\pi\\}\\rangle$$$

Lean4

theorem mono' (h : l₁ ≤ l₂) (hc : c₁ ≤ c₂) (hr : ∀ J ∈ π, r₁ (π.tag J) ≤ r₂ (π.tag J)) (hπ : l₁.MemBaseSet I c₁ r₁ π) :
    l₂.MemBaseSet I c₂ r₂ π :=
  ⟨hπ.1.mono' hr, fun h₂ => hπ.2 (le_iff_imp.1 h.2.1 h₂), fun hD => (hπ.3 (le_iff_imp.1 h.2.2 hD)).trans hc, fun hD =>
    (hπ.4 (le_iff_imp.1 h.2.2 hD)).imp fun _ hπ => ⟨hπ.1, hπ.2.trans hc⟩⟩

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