pi_mono' — Mathlib

English

If t1 i ⊆ t2 i for all i ∈ s₂, and s₂ ⊆ s₁, then s₁.pi t₁ ⊆ s₂.pi t₂.

Русский

Если для всех i ∈ s₂ выполняется t₁ i ⊆ t₂ i, и s₂ ⊆ s₁, то s₁.pi t₁ ⊆ s₂.pi t₂.

LaTeX

$$$ \text{(pi}\_m o n o'\text{)}} : \forall i, i\in s₂ \to t₁ i \subseteq t₂ i \; \land \; s₂ \subseteq s₁ \Rightarrow s₁.pi t₁ \subseteq s₂.pi t₂ $$$

Lean4

@[gcongr]
theorem pi_mono' (h : ∀ i ∈ s₂, t₁ i ⊆ t₂ i) (h' : s₂ ⊆ s₁) : pi s₁ t₁ ⊆ pi s₂ t₂ := fun _ hx i hi ↦
  h i hi (hx i (h' hi))

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