sdiff_eq_sdiff_iff_inf_eq_inf — Mathlib

English

Two sdiffs are equal if and only if their infima with a common element agree: y \ x = y \ z ↔ y ∧ x = y ∧ z.

Русский

Два разности SDiff равны тогда и только тогда, когда их инфимы с общим элементом совпадают: y \ x = y \ z ↔ y ∩ x = y ∩ z.

LaTeX

$$$y \setminus x = y \setminus z \iff (y \wedge x) = (y \wedge z)$$$

Lean4

theorem sdiff_eq_sdiff_iff_inf_eq_inf : y \ x = y \ z ↔ y ⊓ x = y ⊓ z :=
  ⟨fun h =>
    eq_of_inf_eq_sup_eq (a := y \ x) (by rw [inf_inf_sdiff, h, inf_inf_sdiff])
      (by rw [sup_inf_sdiff, h, sup_inf_sdiff]),
    fun h => by rw [← sdiff_inf_self_right, ← sdiff_inf_self_right z y, inf_comm, h, inf_comm]⟩

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