Skip to content

Commit

Permalink
feat(Order/WithBot): add forall_iff_eq_bot and forall_iff_eq_top (
Browse files Browse the repository at this point in the history
#14169)

- [x] Add `forall_iff_eq_bot `
- [x] Add `forall_iff_eq_top `

Co-authored-by: @D-Thomine
  • Loading branch information
pitmonticone committed Jul 3, 2024
1 parent ea932ed commit b35dfa6
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 4 deletions.
4 changes: 4 additions & 0 deletions Mathlib/Data/Option/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -485,4 +485,8 @@ lemma isNone_eq_false_iff (a : Option α) : Option.isNone a = false ↔ Option.i
lemma eq_none_or_eq_some (a : Option α) : a = none ∨ ∃ x, a = some x :=
Option.exists.mp exists_eq'

lemma forall_some_ne_iff_eq_none {o : Option α} : (∀ (x : α), some x ≠ o) ↔ o = none := by
apply not_iff_not.1
simpa only [not_forall, not_not] using Option.ne_none_iff_exists.symm

end Option
19 changes: 15 additions & 4 deletions Mathlib/Order/WithBot.lean
Original file line number Diff line number Diff line change
Expand Up @@ -182,10 +182,12 @@ lemma map₂_coe_coe (f : α → β → γ) (a : α) (b : β) : map₂ f a b = f
@[simp] lemma map₂_eq_bot_iff {f : α → β → γ} {a : WithBot α} {b : WithBot β} :
map₂ f a b = ⊥ ↔ a = ⊥ ∨ b = ⊥ := Option.map₂_eq_none_iff

theorem ne_bot_iff_exists {x : WithBot α} : x ≠ ⊥ ↔ ∃ a : α, ↑a = x :=
Option.ne_none_iff_exists
lemma ne_bot_iff_exists {x : WithBot α} : x ≠ ⊥ ↔ ∃ a : α, ↑a = x := Option.ne_none_iff_exists
#align with_bot.ne_bot_iff_exists WithBot.ne_bot_iff_exists

lemma forall_ne_iff_eq_bot {x : WithBot α} : (∀ a : α, ↑a ≠ x) ↔ x = ⊥ :=
Option.forall_some_ne_iff_eq_none

/-- Deconstruct a `x : WithBot α` to the underlying value in `α`, given a proof that `x ≠ ⊥`. -/
def unbot : ∀ x : WithBot α, x ≠ ⊥ → α | (x : α), _ => x
#align with_bot.unbot WithBot.unbot
Expand Down Expand Up @@ -837,10 +839,12 @@ theorem ofDual_map (f : αᵒᵈ → βᵒᵈ) (a : WithTop αᵒᵈ) :
rfl
#align with_top.of_dual_map WithTop.ofDual_map

theorem ne_top_iff_exists {x : WithTop α} : x ≠ ⊤ ↔ ∃ a : α, ↑a = x :=
Option.ne_none_iff_exists
lemma ne_top_iff_exists {x : WithTop α} : x ≠ ⊤ ↔ ∃ a : α, ↑a = x := Option.ne_none_iff_exists
#align with_top.ne_top_iff_exists WithTop.ne_top_iff_exists

lemma forall_ne_iff_eq_top {x : WithTop α} : (∀ a : α, ↑a ≠ x) ↔ x = ⊤ :=
Option.forall_some_ne_iff_eq_none

/-- Deconstruct a `x : WithTop α` to the underlying value in `α`, given a proof that `x ≠ ⊤`. -/
def untop : ∀ x : WithTop α, x ≠ ⊤ → α | (x : α), _ => x
#align with_top.untop WithTop.untop
Expand Down Expand Up @@ -1067,6 +1071,10 @@ theorem ofDual_map (f : αᵒᵈ → βᵒᵈ) (a : WithBot αᵒᵈ) :
rfl
#align with_bot.of_dual_map WithBot.ofDual_map

lemma forall_lt_iff_eq_bot [Preorder α] {x : WithBot α} :
(∀ y : α, x < y) ↔ x = ⊥ :=
fun h ↦ forall_ne_iff_eq_bot.mp (fun x ↦ (h x).ne'), fun h ↦ h ▸ fun y ↦ bot_lt_coe y⟩

section LE

variable [LE α] {a b : α}
Expand Down Expand Up @@ -1264,6 +1272,9 @@ theorem coe_untop'_le (a : WithTop α) (b : α) : a.untop' b ≤ a :=
theorem coe_top_lt [OrderTop α] {x : WithTop α} : (⊤ : α) < x ↔ x = ⊤ :=
WithBot.lt_coe_bot (α := αᵒᵈ)

lemma forall_lt_iff_eq_top {x : WithTop α} : (∀ y : α, y < x) ↔ x = ⊤ :=
fun h ↦ forall_ne_iff_eq_top.mp (fun x ↦ (h x).ne), fun h ↦ h ▸ fun y ↦ coe_lt_top y⟩

end Preorder

instance semilatticeInf [SemilatticeInf α] : SemilatticeInf (WithTop α) :=
Expand Down

0 comments on commit b35dfa6

Please sign in to comment.