le_iff_eq_sup_sdiff — Mathlib

English

Alternative formulation: under hz hx, x ≤ z is equivalent to y = z ⊔ (y \ x).

Русский

Альтернативная формулировка: при hz hx, x ≤ z эквивалентно y = z ⊔ (y \ x).

LaTeX

$$$hz : z \le y \land hx : x \le y \Rightarrow x \le z \iff y = z \sqcup (y \setminus x)$$$

Lean4

theorem le_iff_eq_sup_sdiff (hz : z ≤ y) (hx : x ≤ y) : x ≤ z ↔ y = z ⊔ y \ x :=
  ⟨fun H => by
    apply le_antisymm
    · conv_lhs => rw [← sup_inf_sdiff y x]
      gcongr
      rwa [inf_eq_right.2 hx]
    · grw [hz]
      rw [sup_sdiff_left], fun H => by
    conv_lhs at H => rw [← sup_sdiff_cancel_right hx]
    refine le_of_inf_le_sup_le ?_ H.le
    rw [inf_sdiff_self_right]
    exact bot_le⟩
    -- cf. `IsCompl.sup_inf`

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