himp_le

Mathlib.Order.BooleanAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#himp_le

English

In a Boolean algebra, x ⇨ y ≤ z is equivalent to y ≤ z and Codisjoint x z.

Русский

В булевой алгебре x ⇨ y ≤ z эквивалентно y ≤ z и Codisjoint x z.

LaTeX

$$x \Rightarrow y \le z \iff y \le z \wedge Codisjoint(x,z)$$

Lean4

theorem himp_le : x ⇨ y ≤ z ↔ y ≤ z ∧ Codisjoint x z :=
  (@le_sdiff αᵒᵈ _ _ _ _).trans <| and_congr_right' <| @codisjoint_comm _ (_) _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru