/
BoolIndicator.lean
61 lines (46 loc) · 2.18 KB
/
BoolIndicator.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
/-
Copyright (c) 2022 Dagur Tómas Ásgeirsson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Dagur Tómas Ásgeirsson, Leonardo de Moura
-/
import Mathlib.Data.Set.Basic
#align_import data.set.bool_indicator from "leanprover-community/mathlib"@"fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e"
/-!
# Indicator function valued in bool
See also `Set.indicator` and `Set.piecewise`.
-/
open Bool
namespace Set
variable {α : Type*} (s : Set α)
/-- `boolIndicator` maps `x` to `true` if `x ∈ s`, else to `false` -/
noncomputable def boolIndicator (x : α) :=
@ite _ (x ∈ s) (Classical.propDecidable _) true false
#align set.bool_indicator Set.boolIndicator
theorem mem_iff_boolIndicator (x : α) : x ∈ s ↔ s.boolIndicator x = true := by
unfold boolIndicator
split_ifs with h <;> simp [h]
#align set.mem_iff_bool_indicator Set.mem_iff_boolIndicator
theorem not_mem_iff_boolIndicator (x : α) : x ∉ s ↔ s.boolIndicator x = false := by
unfold boolIndicator
split_ifs with h <;> simp [h]
#align set.not_mem_iff_bool_indicator Set.not_mem_iff_boolIndicator
theorem preimage_boolIndicator_true : s.boolIndicator ⁻¹' {true} = s :=
ext fun x ↦ (s.mem_iff_boolIndicator x).symm
#align set.preimage_bool_indicator_true Set.preimage_boolIndicator_true
theorem preimage_boolIndicator_false : s.boolIndicator ⁻¹' {false} = sᶜ :=
ext fun x ↦ (s.not_mem_iff_boolIndicator x).symm
#align set.preimage_bool_indicator_false Set.preimage_boolIndicator_false
open scoped Classical
theorem preimage_boolIndicator_eq_union (t : Set Bool) :
s.boolIndicator ⁻¹' t = (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅ := by
ext x
simp only [boolIndicator, mem_preimage]
split_ifs <;> simp [*]
#align set.preimage_bool_indicator_eq_union Set.preimage_boolIndicator_eq_union
theorem preimage_boolIndicator (t : Set Bool) :
s.boolIndicator ⁻¹' t = univ ∨
s.boolIndicator ⁻¹' t = s ∨ s.boolIndicator ⁻¹' t = sᶜ ∨ s.boolIndicator ⁻¹' t = ∅ := by
simp only [preimage_boolIndicator_eq_union]
split_ifs <;> simp [s.union_compl_self]
#align set.preimage_bool_indicator Set.preimage_boolIndicator
end Set