eq_of_mem_uIcc_of_mem_uIcc' — Mathlib

English

In a distributive lattice with locally finite order, if b ∈ [[a,c]] and c ∈ [[a,b]], then b = c.

Русский

В распределённой решётке с локально конечным порядком, если b ∈ [[a,c]] и c ∈ [[a,b]], тогда b = c.

LaTeX

$$$b \in [[a, c]] \rightarrow c \in [[a, b]] \rightarrow b = c$$$

Lean4

theorem eq_of_mem_uIcc_of_mem_uIcc' : b ∈ [[a, c]] → c ∈ [[a, b]] → b = c :=
  by
  simp_rw [mem_uIcc]
  exact Set.eq_of_mem_uIcc_of_mem_uIcc'

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