sdiff_sup_sdiff_cancel' — Mathlib

English

Let hinf: a ⊓ c ≤ b and hsup: b ≤ a ⊔ c. Then a \\ b ⊔ b \\ c = a \\ c.

Русский

Пусть hinf: a ⊓ c ≤ b и hsup: b ≤ a ⊔ c. Тогда a \\ b ⊔ b \\ c = a \\ c.

LaTeX

$$$ a \\\\setminus b \\\\sqcup b \\\\setminus c = a \\\\setminus c $$$

Lean4

/-- a version of `sdiff_sup_sdiff_cancel` with more general hypotheses. -/
theorem sdiff_sup_sdiff_cancel' (hinf : a ⊓ c ≤ b) (hsup : b ≤ a ⊔ c) : a \ b ⊔ b \ c = a \ c :=
  by
  refine (sdiff_triangle ..).antisymm' <| sup_le ?_ <| by simpa [sup_comm]
  rw [← sdiff_inf_self_left (b := c)]
  exact sdiff_le_sdiff_left hinf

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