inf_sdiff_eq_bot_iff — Mathlib

English

Let hz : z ≤ y and hx : x ≤ y. Then z ⊓ (y \ x) = ⊥ if and only if z ≤ x.

Русский

Пусть z ≤ y, x ≤ y. Тогда z ⊓ (y \ x) = ⊥ тогда и только тогда, когда z ≤ x.

LaTeX

$$$(hz : z \le y) (hx : x \le y) : z \wedge (y \setminus x) = \bot \iff z \le x$$$

Lean4

theorem inf_sdiff_eq_bot_iff (hz : z ≤ y) (hx : x ≤ y) : z ⊓ y \ x = ⊥ ↔ z ≤ x :=
  by
  rw [← disjoint_iff]
  exact disjoint_sdiff_iff_le hz hx

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