le_inter — Mathlib

English

The relation s ≤ t ∩ u is equivalent to s ≤ t and s ≤ u: s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u.

Русский

Соотношение s ≤ t ∩ u эквивалентно s ≤ t и s ≤ u: s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u.

LaTeX

$$$s \\le t \\cap u \\;\\iff\\; (s \\le t) \\land (s \\le u).$$$

Lean4

theorem le_inter (h₁ : s ≤ t) (h₂ : s ≤ u) : s ≤ t ∩ u :=
  by
  revert s u; refine @(Multiset.induction_on t ?_ fun a t IH => ?_) <;> intro s u h₁ h₂
  · simpa only [zero_inter] using h₁
  by_cases h : a ∈ u
  · rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons]
    exact IH (erase_le_iff_le_cons.2 h₁) (erase_le_erase _ h₂)
  · rw [cons_inter_of_neg _ h]
    exact IH ((le_cons_of_notMem <| mt (mem_of_le h₂) h).1 h₁) h₂

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