sdiff_sdiff — Mathlib

English

Let α be a generalized Heyting algebra. For all a,b,c ∈ α, (a \ b) \ c = a \ (b ⊔ c).

Русский

Пусть α — обобщенная алгебра Хейтинга. Для любых a, b, c ∈ α выполняется (a \ b) \ c = a \ (b ⊔ c).

LaTeX

$$$ (a \\backslash b) \\backslash c = a \\backslash (b \\sqcup c) $$$

Lean4

theorem sdiff_sdiff (a b c : α) : (a \ b) \ c = a \ (b ⊔ c) :=
  eq_of_forall_ge_iff fun d => by simp_rw [sdiff_le_iff, sup_assoc]

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