instPreorder — Mathlib

English

There is a canonical preorder on the Booleanisation of a generalized Boolean algebra, with the induced less-than relation characterized by standard order-theoretic properties (e.g., x < y iff x ≤ y and not y ≤ x).

Русский

У буллизации обобщённой булевой алгебры существует канонический пред-порядок, где отношение x < y эквивалентно x ≤ y и не (y ≤ x) и т.д.

LaTeX

$$Booleanisation(α) carries a canonical preorder with x < y iff x ≤ y ∧ ¬(y ≤ x).$$

Lean4

instance instPreorder : Preorder (Booleanisation α)
    where
  lt := (· < ·)
  lt_iff_le_not_ge
    | lift a, lift b => by simp [lt_iff_le_not_ge]
    | lift a, comp b => by simp
    | comp a, lift b => by simp
    | comp a, comp b => by simp [lt_iff_le_not_ge]
  le_refl
    | lift _ => LE.lift le_rfl
    | comp _ => LE.comp le_rfl
  le_trans
    | lift _, lift _, lift _, LE.lift hab, LE.lift hbc => LE.lift <| hab.trans hbc
    | lift _, lift _, comp _, LE.lift hab, LE.sep hbc => LE.sep <| hbc.mono_left hab
    | lift _, comp _, comp _, LE.sep hab, LE.comp hcb => LE.sep <| hab.mono_right hcb
    | comp _, comp _, comp _, LE.comp hba, LE.comp hcb => LE.comp <| hcb.trans hba

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