sdiff_triangle — Mathlib

English

Let a, b, c be elements of a generalized co-Heyting algebra. Then a \\ c ≤ (a \\ b) ⊔ (b \\ c).

Русский

Пусть a, b, c — элементы обобщённой коейтинговой алгебры. Тогда a \\ c ≤ (a \\ b) ⊔ (b \\ c).

LaTeX

$$$ a \\\\setminus c \\\\le a \\\\setminus b \\\\vee b \\\\setminus c $$$

Lean4

theorem sdiff_triangle (a b c : α) : a \ c ≤ a \ b ⊔ b \ c :=
  by
  rw [sdiff_le_iff, sup_left_comm, ← sdiff_le_iff]
  exact sdiff_sdiff_le.trans le_sup_sdiff

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