inter_le_right — Mathlib

English

If s ≤ t and s ≤ u, then s ≤ t ∩ u.

Русский

Если s ≤ t и s ≤ u, то s ≤ t ∩ u.

LaTeX

$$$\\text{If } s \\le t \\text{ and } s \\le u, \\text{ then } s \\le t \\cap u.$$$

Lean4

theorem inter_le_right : s ∩ t ≤ t := by
  induction s using Multiset.induction_on generalizing t with
  | empty => exact (zero_inter t).symm ▸ zero_le _
  | cons a s IH =>
    by_cases h : a ∈ t
    · simpa [h] using cons_le_cons a (IH (t := t.erase a))
    · simp [h, IH]

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