ofBoolAlg_mul_ofBoolAlg_eq_left_iff

English

The left-implication property holds in the Boolean ring setting: a ≤ b is equivalent to certain multiplicative relation on their images.

Русский

Левая импликация по булеву кольцу: a ≤ b эквивалентно определённому умножению изображений.

LaTeX

$$$\mathrm{ofBoolAlg}(a) \cdot \mathrm{ofBoolAlg}(b) = \mathrm{ofBoolAlg}(a) \iff a \le b$$$

Lean4

@[simp]
theorem ofBoolAlg_mul_ofBoolAlg_eq_left_iff {a b : AsBoolAlg α} : ofBoolAlg a * ofBoolAlg b = ofBoolAlg a ↔ a ≤ b :=
  @inf_eq_left (AsBoolAlg α) _ _ _

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