comp_eq_right_iff_le — Mathlib

English

For nuclei n and m on a frame X, n ∘ m = m if and only if n ≤ m.

Русский

Для нуклеусов n и m на раме X выполняется: n ∘ m = m тогда и только тогда, когда n ≤ m.

LaTeX

$$$ n \\circ m = m \\ \\iff \\ n \\le m $$$

Lean4

theorem comp_eq_right_iff_le : n ∘ m = m ↔ n ≤ m
    where
  mpr h := funext_iff.mpr <| fun _ ↦ le_antisymm (le_trans (h (m _)) (m.idempotent' _)) le_apply
  mp
    h := by
    rw [← coe_le_coe, ← h]
    exact fun _ ↦ monotone le_apply

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