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₂