le_symmDiff_iff_left — Mathlib

English

Repeatedly, disjointness with symmetric diff is preserved under inf operations: Disjoint (a Δ b) (a ∧ b).

Русский

Несовместность между симмDiff и их пересечением сохраняется при операции inf: Disjoint (a Δ b) (a ∧ b).

LaTeX

$$Disjoint (symmDiff a b) (SemilatticeInf.toMin.min a b)$$

Lean4

@[simp]
theorem le_symmDiff_iff_left : a ≤ a ∆ b ↔ Disjoint a b :=
  by
  refine ⟨fun h => ?_, fun h => h.symmDiff_eq_sup.symm ▸ le_sup_left⟩
  rw [symmDiff_eq_sup_sdiff_inf] at h
  exact disjoint_iff_inf_le.mpr (le_sdiff_right.1 <| inf_le_of_left_le h).le

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