le_induce_union_left — Mathlib

English

The left inequality in le_induce_union holds; the supremum of inductions is below the induction on the union.

Русский

Левая неравенство в le_induce_union выполняется: верхняя граница индукций не превышает индукцию на объединение.

LaTeX

$$$ \\text{theorem } le\\_induce\\_union\_left: G'.induce s \\le G'.induce (s\\cup s') $$$

Lean4

theorem le_induce_union_left : G'.induce s ≤ G'.induce (s ∪ s') := by exact (sup_le_iff.mp le_induce_union).1

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