ne — Mathlib · SciLib

English

Let a, b be elements of a partially ordered set with bottom ⊥. If a is not bottom and a is disjoint from b (i.e., a ∧ b = ⊥), then a ≠ b.

Русский

Пусть a, b лежат в частично упорядоченном множестве с нулем ⊥. Если a ≠ ⊥ и a несоприкасается с b (то есть a ∧ b = ⊥), то a ≠ b.

LaTeX

$$$(a \neq \ bot) \land (a \wedge b = \bot) \Rightarrow a \neq b$$$

Lean4

theorem ne (ha : a ≠ ⊥) (hab : Disjoint a b) : a ≠ b := fun h ↦ ha <| disjoint_self.1 <| by rwa [← h] at hab

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