interedges_mono — Mathlib

English

If s2 ⊆ s1 and t2 ⊆ t1, then interedges(r,s2,t2) ⊆ interedges(r,s1,t1).

Русский

Если s2 ⊆ s1 и t2 ⊆ t1, то interedges(r,s2,t2) ⊆ interedges(r,s1,t1).

LaTeX

$$$ \mathrm{interedges}(r,s2,t2) \subseteq \mathrm{interedges}(r,s1,t1) $$$

Lean4

theorem interedges_mono (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) : interedges r s₂ t₂ ⊆ interedges r s₁ t₁ := fun x ↦
  by
  simp_rw [mem_interedges_iff]
  exact fun h ↦ ⟨hs h.1, ht h.2.1, h.2.2⟩

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