map_eq_bot_iff — Mathlib

English

For any f with an order-isomorphism structure, f(a) = ⊥ iff a = ⊥.

Русский

Для любого f с структурой изоморфизма порядка, f(a) = ⊥ тогда и только тогда, когда a = ⊥.

LaTeX

$$$ f(a) = \bot \iff a = \bot $$$

Lean4

@[simp]
theorem map_eq_bot_iff [LE α] [OrderBot α] [PartialOrder β] [OrderBot β] [OrderIsoClass F α β] (f : F) {a : α} :
    f a = ⊥ ↔ a = ⊥ := by rw [← map_bot f, (EquivLike.injective f).eq_iff]

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