inf_sdiff_assoc — Mathlib

English

Associativity of inf and SDiff: (x ⊓ y) \ z = x ⊓ y \ z.

Русский

Ассоциативность ∧ и SDiff: (x ⊓ y) \ z = x ⊓ (y \ z).

LaTeX

$$$$ (x \land y) \setminus z = x \land y \setminus z $$$$

Lean4

/-- See also `sdiff_inf_right_comm`. -/
theorem inf_sdiff_assoc (x y z : α) : (x ⊓ y) \ z = x ⊓ y \ z :=
  sdiff_unique (by rw [inf_assoc, ← inf_sup_left, sup_inf_sdiff]) <|
    calc
      x ⊓ y ⊓ z ⊓ (x ⊓ y \ z) = x ⊓ x ⊓ (y ⊓ z ⊓ y \ z) := by ac_rfl
      _ = ⊥ := by rw [inf_inf_sdiff, inf_bot_eq]

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