sigma_mono — Mathlib

English

Subset relations are preserved under sigma: if s1 ⊆ s2 and t1 i ⊆ t2 i, then s1.sigma t1 ⊆ s2.sigma t2.

Русский

Относительная подмножество сохраняется под сигма: если S1 ⊆ S2 и T1 i ⊆ T2 i, то S1.sigma T1 ⊆ S2.sigma T2.

LaTeX

$$$s_1 \\subseteq s_2 \\;\\land\\; \\forall i,\\; t_1(i) \\subseteq t_2(i) \\Rightarrow s_1.\\sigma t_1 \\subseteq s_2.\\sigma t_2$$$

Lean4

theorem sigma_mono (hs : s₁ ⊆ s₂) (ht : ∀ i, t₁ i ⊆ t₂ i) : s₁.sigma t₁ ⊆ s₂.sigma t₂ := fun _ hx ↦ ⟨hs hx.1, ht _ hx.2⟩

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