sdiff_unique — Mathlib

English

If x = (x ∧ y) ∨ z and (x ∧ y ∧ z) = ⊥, then x \ y = z; the decomposition of x by y is unique in this situation.

Русский

Если x = (x ∧ y) ∨ z и (x ∧ y ∧ z) = ⊥, то x \ y = z; разбиение x по y уникально в данной ситуации.

LaTeX

$$$(x \wedge y) \vee z = x \wedge (x \wedge y) \wedge z = \bot \Rightarrow x \setminus y = z$$$

Lean4

theorem sdiff_unique (s : x ⊓ y ⊔ z = x) (i : x ⊓ y ⊓ z = ⊥) : x \ y = z :=
  by
  conv_rhs at s => rw [← sup_inf_sdiff x y, sup_comm]
  rw [sup_comm] at s
  conv_rhs at i => rw [← inf_inf_sdiff x y, inf_comm]
  rw [inf_comm] at i
  exact (eq_of_inf_eq_sup_eq i s).symm

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