theorem ite_eq_top {α : Type u_1} [Top α] (h : Prop) [Decidable h] {x y : α} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : (if h then x else y) ≠ ⊤

theorem subtype_val_iSup {ι : Type u_1} {α : Type u_2} [i : Nonempty ι] [ConditionallyCompleteLattice α] {f : ι → α} {a b : α} [Fact (a ≤ b)] (h : ∀ (i : ι), f i ∈ Set.Icc a b) : ↑(⨆ (i : ι), ⟨f i, ⋯⟩) = ⨆ (i : ι), f i

theorem subtype_val_iSup' {ι : Type u_1} {α : Type u_2} [i : Nonempty ι] [ConditionallyCompleteLattice α] {f : ι → α} {a b : α} [Fact (a ≤ b)] (h : ∀ (i : ι), f i ∈ Set.Icc a b) : ⨆ (i : ι), ⟨f i, ⋯⟩ = ⟨⨆ (i : ι), f i, ⋯⟩

theorem subtype_val_iInf {ι : Type u_1} {α : Type u_2} [i : Nonempty ι] [ConditionallyCompleteLattice α] {f : ι → α} {a b : α} [Fact (a ≤ b)] (h : ∀ (i : ι), f i ∈ Set.Icc a b) : ↑(⨅ (i : ι), ⟨f i, ⋯⟩) = ⨅ (i : ι), f i

theorem subtype_val_iInf' {ι : Type u_1} {α : Type u_2} [i : Nonempty ι] [ConditionallyCompleteLattice α] {f : ι → α} {a b : α} [Fact (a ≤ b)] (h : ∀ (i : ι), f i ∈ Set.Icc a b) : ⨅ (i : ι), ⟨f i, ⋯⟩ = ⟨⨅ (i : ι), f i, ⋯⟩

theorem ENNReal.bdd_le_mul_tendsto_zero {α : Type u_1} {l : Filter α} {f g : α → ENNReal} {b : ENNReal} (hb : b ≠ ⊤) (hf : Filter.Tendsto f l (nhds 0)) (hg : ∀ᶠ (x : α) in l, g x ≤ b) : Filter.Tendsto (fun (x : α) => f x * g x) l (nhds 0)

Analogous to bdd_le_mul_tendsto_zero, for ENNReal (which otherwise lacks a continuous multiplication function). The product of a sequence that tends to zero with any bounded sequence also tends to zero.

theorem csInf_mul_nonneg {s t : Set ℝ} (hs₀ : s.Nonempty) (hs₁ : ∀ x ∈ s, 0 ≤ x) (ht₀ : t.Nonempty) (ht₁ : ∀ x ∈ t, 0 ≤ x) : sInf (s * t) = sInf s * sInf t

theorem Multiset.map_univ_eq_iff {α : Type u_1} {β : Type u_2} [Fintype α] (f g : α → β) : map f Finset.univ.val = map g Finset.univ.val ↔ ∃ (e : α ≃ α), f = g ∘ ⇑e

If two functions from finite types have the same multiset of values, there exists a bijection between the domains that commutes with the functions.

theorem exists_equiv_of_multiset_map_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [DecidableEq γ] (f : α → γ) (g : β → γ) (h : Multiset.map f Finset.univ.val = Multiset.map g Finset.univ.val) : ∃ (e : α ≃ β), f = g ∘ ⇑e

If two functions from finite types have the same multiset of values, there exists a bijection between the domains that commutes with the functions.